Theorem an12s

Swap two conjuncts in antecedent. The label suffix "s" means that an12 is combined with syl (or a variant). (Contributed by NM, 13-Mar-1996.)

Hypothesis
an12s.1
\( \vdash \varphi \wedge (\psi \wedge \chi) \rightarrow \theta \)
Conclusion
\( \vdash \psi \wedge (\varphi \wedge \chi) \rightarrow \theta \)
Proof
l0
an12
\( \vdash \psi \wedge (\varphi \wedge \chi) \leftrightarrow \varphi \wedge (\psi \wedge \chi) \)
an12s.1
\( \vdash \varphi \wedge (\psi \wedge \chi) \rightarrow \theta \)
sylbi l0 _