Metamath Proof Explorer

Theorem 13an22anassOLD

Description: Obsolete version of 13an22anass as of 31-Oct-2026. (Contributed by Thierry Arnoux, 21-Jan-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 13an22anassOLD 
|- ( ( 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 ) ) )