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