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