This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 4anpull2

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

Ref Expression
Assertion 4anpull2 
|- ( ( ( 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 ) )