Metamath Proof Explorer

Theorem anan

Description: Multiple commutations in conjunction. (Contributed by Peter Mazsa, 7-Mar-2020)

Ref Expression
Assertion anan 
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ ( ( ph /\ th ) /\ ta ) ) <-> ( ( ps /\ th ) /\ ( ph /\ ( ch /\ ta ) ) ) )

Proof

Step Hyp Ref Expression
1 an4 
 |-  ( ( ( ( ph /\ ps ) /\ ch ) /\ ( ( ph /\ th ) /\ ta ) ) <-> ( ( ( ph /\ ps ) /\ ( ph /\ th ) ) /\ ( ch /\ ta ) ) )
2 anandi 
 |-  ( ( ph /\ ( ps /\ th ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ th ) ) )
3 ancom 
 |-  ( ( ph /\ ( ps /\ th ) ) <-> ( ( ps /\ th ) /\ ph ) )
4 2 3 bitr3i 
 |-  ( ( ( ph /\ ps ) /\ ( ph /\ th ) ) <-> ( ( ps /\ th ) /\ ph ) )
5 4 anbi1i 
 |-  ( ( ( ( ph /\ ps ) /\ ( ph /\ th ) ) /\ ( ch /\ ta ) ) <-> ( ( ( ps /\ th ) /\ ph ) /\ ( ch /\ ta ) ) )
6 anass 
 |-  ( ( ( ( ps /\ th ) /\ ph ) /\ ( ch /\ ta ) ) <-> ( ( ps /\ th ) /\ ( ph /\ ( ch /\ ta ) ) ) )
7 1 5 6 3bitri 
 |-  ( ( ( ( ph /\ ps ) /\ ch ) /\ ( ( ph /\ th ) /\ ta ) ) <-> ( ( ps /\ th ) /\ ( ph /\ ( ch /\ ta ) ) ) )