Metamath Proof Explorer

Theorem 4an21

Description: Rearrangement of 4 conjuncts with a triple conjunction. (Contributed by AV, 4-Mar-2022)

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

Proof

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