Metamath Proof Explorer

Theorem 13an22anass

Description: Associative law for four conjunctions with a triple conjunction. (Contributed by Thierry Arnoux, 21-Jan-2025)

Ref Expression
Assertion 13an22anass 
|- ( ( ph /\ ( ps /\ ch /\ th ) ) <-> ( ( ph /\ ps ) /\ ( ch /\ th ) ) )

Proof

Step Hyp Ref Expression
1 an2anr 
 |-  ( ( ( ps /\ ch ) /\ ( th /\ ph ) ) <-> ( ( ch /\ ps ) /\ ( ph /\ th ) ) )
2 an2anr 
 |-  ( ( ( ph /\ ch ) /\ ( th /\ ps ) ) <-> ( ( ch /\ ph ) /\ ( ps /\ th ) ) )
3 an4 
 |-  ( ( ( ch /\ ph ) /\ ( ps /\ th ) ) <-> ( ( ch /\ ps ) /\ ( ph /\ th ) ) )
4 2 3 bitri 
 |-  ( ( ( ph /\ ch ) /\ ( th /\ ps ) ) <-> ( ( ch /\ ps ) /\ ( ph /\ th ) ) )
5 an43 
 |-  ( ( ( ph /\ ch ) /\ ( th /\ ps ) ) <-> ( ( ph /\ ps ) /\ ( ch /\ th ) ) )
6 1 4 5 3bitr2ri 
 |-  ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ps /\ ch ) /\ ( th /\ ph ) ) )
7 3an4anass 
 |-  ( ( ( ps /\ ch /\ th ) /\ ph ) <-> ( ( ps /\ ch ) /\ ( th /\ ph ) ) )
8 ancom 
 |-  ( ( ( ps /\ ch /\ th ) /\ ph ) <-> ( ph /\ ( ps /\ ch /\ th ) ) )
9 6 7 8 3bitr2ri 
 |-  ( ( ph /\ ( ps /\ ch /\ th ) ) <-> ( ( ph /\ ps ) /\ ( ch /\ th ) ) )