3anim123d Show Code edit
# Deduction joining 3 implications to form implication of conjunctions.
thm (3anim123d () (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 anim12d 3anim123d.3 anim12d ps th et df-3an ch ta ze df-3an 3imtr4g)
(-> ph (-> (/\/\ ps th et) (/\/\ ch ta ze)))
edit