3adant1 Show Code edit
# Deduction adding a conjunct to antecedent.
thm (3adant1 () (3adant.1 (-> (/\ ph ps) ch)) (-> (/\/\ th ph ps) ch) th ph ps 3simpc 3adant.1 syl)
(-> (/\/\ th ph ps) ch)
edit