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