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