Theorem ancom2s

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

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