Theorem 4anpull2OLD

Obsolete version of 4anpull2 as of 26-Jun-2026. 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 modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \leftrightarrow (\varphi \wedge \chi \wedge \theta) \wedge \psi \)
Proof
l0
anass
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \leftrightarrow \varphi \wedge (\psi \wedge (\chi \wedge \theta)) \)
l1
anass
\( \vdash \varphi \wedge (\chi \wedge \theta) \wedge \psi \leftrightarrow \varphi \wedge (\chi \wedge \theta \wedge \psi) \)
3anass
l3
anbi1i _
\( \vdash (\varphi \wedge \chi \wedge \theta) \wedge \psi \leftrightarrow \varphi \wedge (\chi \wedge \theta) \wedge \psi \)
ancom
anbi2i _
\( \vdash \varphi \wedge (\psi \wedge (\chi \wedge \theta)) \leftrightarrow \varphi \wedge (\chi \wedge \theta \wedge \psi) \)
3bitr4ri l1 l3 _
\( \vdash \varphi \wedge (\psi \wedge (\chi \wedge \theta)) \leftrightarrow (\varphi \wedge \chi \wedge \theta) \wedge \psi \)
bitri l0 _