3ad2ant1 Show Code edit
# Deduction adding conjuncts to an antecedent.
thm (3ad2ant1 () (3ad2ant.1 (-> ph ch)) (-> (/\/\ ph ps th) ch) 3ad2ant.1 th adantr ps 3adant2)
(-> (/\/\ ph ps th) ch)
edit