Metamath Proof Explorer

Theorem an33reanOLD

Description: Obsolete version of an33rean as of 21-Apr-2024. (Contributed by Thierry Arnoux, 14-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion an33reanOLD 
|- ( ( ( ph /\ ps /\ ch ) /\ ( th /\ ta /\ et ) /\ ( ze /\ si /\ rh ) ) <-> ( ( ph /\ ta /\ rh ) /\ ( ( ps /\ th ) /\ ( et /\ si ) /\ ( ch /\ ze ) ) ) )

Proof

Step Hyp Ref Expression
1 3anass 
 |-  ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
2 3anan12 
 |-  ( ( th /\ ta /\ et ) <-> ( ta /\ ( th /\ et ) ) )
3 3anrev 
 |-  ( ( ze /\ si /\ rh ) <-> ( rh /\ si /\ ze ) )
4 3anass 
 |-  ( ( rh /\ si /\ ze ) <-> ( rh /\ ( si /\ ze ) ) )
5 3 4 bitri 
 |-  ( ( ze /\ si /\ rh ) <-> ( rh /\ ( si /\ ze ) ) )
6 1 2 5 3anbi123i 
 |-  ( ( ( ph /\ ps /\ ch ) /\ ( th /\ ta /\ et ) /\ ( ze /\ si /\ rh ) ) <-> ( ( ph /\ ( ps /\ ch ) ) /\ ( ta /\ ( th /\ et ) ) /\ ( rh /\ ( si /\ ze ) ) ) )
7 3an6 
 |-  ( ( ( ph /\ ( ps /\ ch ) ) /\ ( ta /\ ( th /\ et ) ) /\ ( rh /\ ( si /\ ze ) ) ) <-> ( ( ph /\ ta /\ rh ) /\ ( ( ps /\ ch ) /\ ( th /\ et ) /\ ( si /\ ze ) ) ) )
8 an4 
 |-  ( ( ( th /\ et ) /\ ( si /\ ze ) ) <-> ( ( th /\ si ) /\ ( et /\ ze ) ) )
9 8 anbi2i 
 |-  ( ( ( ps /\ ch ) /\ ( ( th /\ et ) /\ ( si /\ ze ) ) ) <-> ( ( ps /\ ch ) /\ ( ( th /\ si ) /\ ( et /\ ze ) ) ) )
10 3anass 
 |-  ( ( ( ps /\ ch ) /\ ( th /\ et ) /\ ( si /\ ze ) ) <-> ( ( ps /\ ch ) /\ ( ( th /\ et ) /\ ( si /\ ze ) ) ) )
11 3anass 
 |-  ( ( ( ps /\ ch ) /\ ( th /\ si ) /\ ( et /\ ze ) ) <-> ( ( ps /\ ch ) /\ ( ( th /\ si ) /\ ( et /\ ze ) ) ) )
12 9 10 11 3bitr4i 
 |-  ( ( ( ps /\ ch ) /\ ( th /\ et ) /\ ( si /\ ze ) ) <-> ( ( ps /\ ch ) /\ ( th /\ si ) /\ ( et /\ ze ) ) )
13 an4 
 |-  ( ( ( ps /\ ch ) /\ ( th /\ si ) ) <-> ( ( ps /\ th ) /\ ( ch /\ si ) ) )
14 13 anbi1i 
 |-  ( ( ( ( ps /\ ch ) /\ ( th /\ si ) ) /\ ( et /\ ze ) ) <-> ( ( ( ps /\ th ) /\ ( ch /\ si ) ) /\ ( et /\ ze ) ) )
15 df-3an 
 |-  ( ( ( ps /\ ch ) /\ ( th /\ si ) /\ ( et /\ ze ) ) <-> ( ( ( ps /\ ch ) /\ ( th /\ si ) ) /\ ( et /\ ze ) ) )
16 df-3an 
 |-  ( ( ( ps /\ th ) /\ ( ch /\ si ) /\ ( et /\ ze ) ) <-> ( ( ( ps /\ th ) /\ ( ch /\ si ) ) /\ ( et /\ ze ) ) )
17 14 15 16 3bitr4i 
 |-  ( ( ( ps /\ ch ) /\ ( th /\ si ) /\ ( et /\ ze ) ) <-> ( ( ps /\ th ) /\ ( ch /\ si ) /\ ( et /\ ze ) ) )
18 3ancomb 
 |-  ( ( ps /\ ch /\ et ) <-> ( ps /\ et /\ ch ) )
19 18 anbi1i 
 |-  ( ( ( ps /\ ch /\ et ) /\ ( th /\ si /\ ze ) ) <-> ( ( ps /\ et /\ ch ) /\ ( th /\ si /\ ze ) ) )
20 3an6 
 |-  ( ( ( ps /\ th ) /\ ( ch /\ si ) /\ ( et /\ ze ) ) <-> ( ( ps /\ ch /\ et ) /\ ( th /\ si /\ ze ) ) )
21 3an6 
 |-  ( ( ( ps /\ th ) /\ ( et /\ si ) /\ ( ch /\ ze ) ) <-> ( ( ps /\ et /\ ch ) /\ ( th /\ si /\ ze ) ) )
22 19 20 21 3bitr4i 
 |-  ( ( ( ps /\ th ) /\ ( ch /\ si ) /\ ( et /\ ze ) ) <-> ( ( ps /\ th ) /\ ( et /\ si ) /\ ( ch /\ ze ) ) )
23 12 17 22 3bitri 
 |-  ( ( ( ps /\ ch ) /\ ( th /\ et ) /\ ( si /\ ze ) ) <-> ( ( ps /\ th ) /\ ( et /\ si ) /\ ( ch /\ ze ) ) )
24 23 anbi2i 
 |-  ( ( ( ph /\ ta /\ rh ) /\ ( ( ps /\ ch ) /\ ( th /\ et ) /\ ( si /\ ze ) ) ) <-> ( ( ph /\ ta /\ rh ) /\ ( ( ps /\ th ) /\ ( et /\ si ) /\ ( ch /\ ze ) ) ) )
25 6 7 24 3bitri 
 |-  ( ( ( ph /\ ps /\ ch ) /\ ( th /\ ta /\ et ) /\ ( ze /\ si /\ rh ) ) <-> ( ( ph /\ ta /\ rh ) /\ ( ( ps /\ th ) /\ ( et /\ si ) /\ ( ch /\ ze ) ) ) )