Metamath Proof Explorer

Theorem an33rean

Description: Rearrange a 9-fold conjunction. (Contributed by Thierry Arnoux, 14-Apr-2019) (Proof shortened by Wolf Lammen, 21-Apr-2024)

Ref Expression
Assertion an33rean 
|- ( ( ( 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 anass 
 |-  ( ( ( th /\ et ) /\ si ) <-> ( th /\ ( et /\ si ) ) )
9 8 anbi2i 
 |-  ( ( ( ps /\ ch ) /\ ( ( th /\ et ) /\ si ) ) <-> ( ( ps /\ ch ) /\ ( th /\ ( et /\ si ) ) ) )
10 an42 
 |-  ( ( ( ps /\ ch ) /\ ( th /\ ( et /\ si ) ) ) <-> ( ( ps /\ th ) /\ ( ( et /\ si ) /\ ch ) ) )
11 9 10 bitri 
 |-  ( ( ( ps /\ ch ) /\ ( ( th /\ et ) /\ si ) ) <-> ( ( ps /\ th ) /\ ( ( et /\ si ) /\ ch ) ) )
12 anass 
 |-  ( ( ( ( ps /\ ch ) /\ ( th /\ et ) ) /\ si ) <-> ( ( ps /\ ch ) /\ ( ( th /\ et ) /\ si ) ) )
13 anass 
 |-  ( ( ( ( ps /\ th ) /\ ( et /\ si ) ) /\ ch ) <-> ( ( ps /\ th ) /\ ( ( et /\ si ) /\ ch ) ) )
14 11 12 13 3bitr4i 
 |-  ( ( ( ( ps /\ ch ) /\ ( th /\ et ) ) /\ si ) <-> ( ( ( ps /\ th ) /\ ( et /\ si ) ) /\ ch ) )
15 14 anbi1i 
 |-  ( ( ( ( ( ps /\ ch ) /\ ( th /\ et ) ) /\ si ) /\ ze ) <-> ( ( ( ( ps /\ th ) /\ ( et /\ si ) ) /\ ch ) /\ ze ) )
16 anass 
 |-  ( ( ( ( ( ps /\ ch ) /\ ( th /\ et ) ) /\ si ) /\ ze ) <-> ( ( ( ps /\ ch ) /\ ( th /\ et ) ) /\ ( si /\ ze ) ) )
17 anass 
 |-  ( ( ( ( ( ps /\ th ) /\ ( et /\ si ) ) /\ ch ) /\ ze ) <-> ( ( ( ps /\ th ) /\ ( et /\ si ) ) /\ ( ch /\ ze ) ) )
18 15 16 17 3bitr3i 
 |-  ( ( ( ( ps /\ ch ) /\ ( th /\ et ) ) /\ ( si /\ ze ) ) <-> ( ( ( ps /\ th ) /\ ( et /\ si ) ) /\ ( ch /\ ze ) ) )
19 df-3an 
 |-  ( ( ( ps /\ ch ) /\ ( th /\ et ) /\ ( si /\ ze ) ) <-> ( ( ( ps /\ ch ) /\ ( th /\ et ) ) /\ ( si /\ ze ) ) )
20 df-3an 
 |-  ( ( ( ps /\ th ) /\ ( et /\ si ) /\ ( ch /\ ze ) ) <-> ( ( ( ps /\ th ) /\ ( et /\ si ) ) /\ ( ch /\ ze ) ) )
21 18 19 20 3bitr4i 
 |-  ( ( ( ps /\ ch ) /\ ( th /\ et ) /\ ( si /\ ze ) ) <-> ( ( ps /\ th ) /\ ( et /\ si ) /\ ( ch /\ ze ) ) )
22 21 anbi2i 
 |-  ( ( ( ph /\ ta /\ rh ) /\ ( ( ps /\ ch ) /\ ( th /\ et ) /\ ( si /\ ze ) ) ) <-> ( ( ph /\ ta /\ rh ) /\ ( ( ps /\ th ) /\ ( et /\ si ) /\ ( ch /\ ze ) ) ) )
23 6 7 22 3bitri 
 |-  ( ( ( ph /\ ps /\ ch ) /\ ( th /\ ta /\ et ) /\ ( ze /\ si /\ rh ) ) <-> ( ( ph /\ ta /\ rh ) /\ ( ( ps /\ th ) /\ ( et /\ si ) /\ ( ch /\ ze ) ) ) )