3anim123i Show Code edit
# Join antecedents and consequents with conjunction.
thm (3anim123i () (3anim123i.1 (-> ph ps) 3anim123i.2 (-> ch th) 3anim123i.3 (-> ta et)) (-> (/\/\ ph ch ta) (/\/\ ps th et)) 3anim123i.1 3anim123i.2 anim12i 3anim123i.3 anim12i ph ch ta df-3an ps th et df-3an 3imtr4i)
(-> (/\/\ ph ch ta) (/\/\ ps th et))
edit