3jaoi Show Code edit
# Disjunction of 3 antecedents (inference).
thm (3jaoi () (3jaoi.1 (-> ph ps) 3jaoi.2 (-> ch ps) 3jaoi.3 (-> th ps)) (-> (\/\/ ph ch th) ps) 3jaoi.1 3jaoi.2 3jaoi.3 3pm3.2i ph ps ch th 3jao ax-mp)
(-> (\/\/ ph ch th) ps)
edit