Metamath Proof Explorer

Theorem 4anpull2OLD

Description: 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.)

Ref Expression
Assertion 4anpull2OLD 
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch /\ th ) /\ ps ) )

Proof

Step Hyp Ref Expression
1 anass 
 |-  ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ph /\ ( ps /\ ( ch /\ th ) ) ) )
2 anass 
 |-  ( ( ( ph /\ ( ch /\ th ) ) /\ ps ) <-> ( ph /\ ( ( ch /\ th ) /\ ps ) ) )
3 3anass 
 |-  ( ( ph /\ ch /\ th ) <-> ( ph /\ ( ch /\ th ) ) )
4 3 anbi1i 
 |-  ( ( ( ph /\ ch /\ th ) /\ ps ) <-> ( ( ph /\ ( ch /\ th ) ) /\ ps ) )
5 ancom 
 |-  ( ( ps /\ ( ch /\ th ) ) <-> ( ( ch /\ th ) /\ ps ) )
6 5 anbi2i 
 |-  ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) <-> ( ph /\ ( ( ch /\ th ) /\ ps ) ) )
7 2 4 6 3bitr4ri 
 |-  ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) <-> ( ( ph /\ ch /\ th ) /\ ps ) )
8 1 7 bitri 
 |-  ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch /\ th ) /\ ps ) )