Generalized Modus Ponens For atomic sentences si, si" and r, where there is a substitution T such that subst(T,si")=subst(T,si) for all i: s1",s2",...,sn",(s1^s2^...^sn => r) implies subst(T,r) A; '(implies (and ' A ')' q ')' |- q;; (Sent A q)