3com12 Show Code edit
# Commutation in antecedent. Swap 1st and 3rd.
thm (3com12 () (3exp.1 (-> (/\/\ ph ps ch) th)) (-> (/\/\ ps ph ch) th) 3exp.1 3exp com12 3imp)
(-> (/\/\ ps ph ch) th)
edit