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