ad2ant2r Show Code edit
# Deduction adding two conjuncts to antecedent.
## Add Conjuncts
thm (ad2ant2r () (ad2ant2.1 (-> (/\ ph ps) ch)) (-> (/\ (/\ ph th) (/\ ps ta)) ch) ad2ant2.1 ta adantrr th adantlr)
(-> (/\ (/\ ph th) (/\ ps ta)) ch)
edit