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