Theorem an4s

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

Hypothesis
an4s.1
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \rightarrow \tau \)
Conclusion
\( \vdash \varphi \wedge \chi \wedge (\psi \wedge \theta) \rightarrow \tau \)
Proof
l0
an4
\( \vdash \varphi \wedge \chi \wedge (\psi \wedge \theta) \leftrightarrow \varphi \wedge \psi \wedge (\chi \wedge \theta) \)
an4s.1
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \rightarrow \tau \)
sylbi l0 _