Theorem ancom1s

Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis
an32s.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \psi \wedge \varphi \wedge \chi \rightarrow \theta \)
Proof
l0
pm3.22
\( \vdash \psi \wedge \varphi \rightarrow \varphi \wedge \psi \)
an32s.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
sylan l0 _