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