Theorem 4anpull2

An equivalence of two four-terms conjunctions with the terms regrouped (here, the second sub-conjunct of the first term is pulled separately). (Contributed by Zhi Wang, 4-Sep-2024.) (Proof shortened by Garrett Katz, 26-Jun-2026.)

Conclusion
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \leftrightarrow (\varphi \wedge \chi \wedge \theta) \wedge \psi \)
Proof
l0
an42
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \leftrightarrow \varphi \wedge \chi \wedge (\theta \wedge \psi) \)
3an4anass
\( \vdash (\varphi \wedge \chi \wedge \theta) \wedge \psi \leftrightarrow \varphi \wedge \chi \wedge (\theta \wedge \psi) \)
bitr4i l0 _