3jao Show Code edit
# Disjunction of 3 antecedents.
thm (3jao () () (-> (/\/\ (-> ph ps) (-> ch ps) (-> th ps)) (-> (\/\/ ph ch th) ps)) ph ps ch jao (\/ ph ch) ps th jao syl6 3imp ph ch th df-3or syl5ib)
(-> (/\/\ (-> ph ps) (-> ch ps) (-> th ps)) (-> (\/\/ ph ch th) ps))
edit