3ad2antr3 Show Code edit
# Deduction adding a conjuncts to antecedent.
thm (3ad2antr3 () (3ad2antl.1 (-> (/\ ph ch) th)) (-> (/\ ph (/\/\ ps ta ch)) th) 3ad2antl.1 ta adantrl ps 3adantr1)
(-> (/\ ph (/\/\ ps ta ch)) th)
edit