3orim123d Show Code edit
# Deduction joining 3 implications to form implication of disjunctions.
thm (3orim123d () (3anim123d.1 (-> ph (-> ps ch)) 3anim123d.2 (-> ph (-> th ta)) 3anim123d.3 (-> ph (-> et ze))) (-> ph (-> (\/\/ ps th et) (\/\/ ch ta ze))) 3anim123d.1 3anim123d.2 orim12d 3anim123d.3 orim12d ps th et df-3or ch ta ze df-3or 3imtr4g)
(-> ph (-> (\/\/ ps th et) (\/\/ ch ta ze)))
edit