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