Theorem an42ds

Inference exchanging the last antecedent with the second one. See also an32s. (Contributed by Thierry Arnoux, 3-Jun-2025.)

Hypothesis
an42ds.1
\( \vdash \varphi \wedge \psi \wedge \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \wedge \theta \wedge \chi \wedge \psi \rightarrow \tau \)
Proof
an32
l1
anbi1i _
\( \vdash \varphi \wedge \psi \wedge \theta \wedge \chi \leftrightarrow \varphi \wedge \theta \wedge \psi \wedge \chi \)
l2
an32
\( \vdash \varphi \wedge \psi \wedge \theta \wedge \chi \leftrightarrow \varphi \wedge \psi \wedge \chi \wedge \theta \)
an32
\( \vdash \varphi \wedge \theta \wedge \psi \wedge \chi \leftrightarrow \varphi \wedge \theta \wedge \chi \wedge \psi \)
l4
3bitr3i l1 l2 _
\( \vdash \varphi \wedge \psi \wedge \chi \wedge \theta \leftrightarrow \varphi \wedge \theta \wedge \chi \wedge \psi \)
an42ds.1
\( \vdash \varphi \wedge \psi \wedge \chi \wedge \theta \rightarrow \tau \)
sylbir l4 _