3jaoian Show Code edit
# Disjunction of 3 antecedents (inference).
thm (3jaoian () (3jaoian.1 (-> (/\ ph ps) ch) 3jaoian.2 (-> (/\ th ps) ch) 3jaoian.3 (-> (/\ ta ps) ch)) (-> (/\ (\/\/ ph th ta) ps) ch) 3jaoian.1 ex 3jaoian.2 ex 3jaoian.3 ex 3jaoi imp)
(-> (/\ (\/\/ ph th ta) ps) ch)
edit