Theorem an42s

Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)

Hypothesis
an41r3s.1
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \rightarrow \tau \)
Conclusion
\( \vdash \varphi \wedge \chi \wedge (\theta \wedge \psi) \rightarrow \tau \)
Proof
an41r3s.1
an4s _
ancom2s _