jao Show Code edit
# Disjunction of antecedents. Compare Theorem *3.44 of
# [bib/WhiteheadRussell] p. 113.
## Disjunction of antecedents
thm (jao () () (-> (-> ph ps) (-> (-> ch ps) (-> (\/ ph ch) ps))) ph ps con3 (-. ps) (-. ph) (-. ch) pm3.43i ps (/\ (-. ph) (-. ch)) con1 syl6 ph ch oran syl7ib ch ps con3 syl5 syl)
(-> (-> ph ps) (-> (-> ch ps) (-> (\/ ph ch) ps)))
edit