Metamath Proof Explorer

Theorem prtlem70

Description: Lemma for prter3 : a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010)

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

Proof

Step Hyp Ref Expression
1 anass 
 |-  ( ( ( ( ph /\ ps ) /\ ( ph /\ th ) ) /\ ( ch /\ ta ) ) <-> ( ( ph /\ ps ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) )
2 1 anbi1i 
 |-  ( ( ( ( ( ph /\ ps ) /\ ( ph /\ th ) ) /\ ( ch /\ ta ) ) /\ et ) <-> ( ( ( ph /\ ps ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) /\ et ) )
3 anandi 
 |-  ( ( ph /\ ( ps /\ th ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ th ) ) )
4 3 anbi1i 
 |-  ( ( ( ph /\ ( ps /\ th ) ) /\ ( ch /\ ta ) ) <-> ( ( ( ph /\ ps ) /\ ( ph /\ th ) ) /\ ( ch /\ ta ) ) )
5 4 anbi1i 
 |-  ( ( ( ( ph /\ ( ps /\ th ) ) /\ ( ch /\ ta ) ) /\ et ) <-> ( ( ( ( ph /\ ps ) /\ ( ph /\ th ) ) /\ ( ch /\ ta ) ) /\ et ) )
6 anass 
 |-  ( ( ( ph /\ ( ps /\ et ) ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) <-> ( ph /\ ( ( ps /\ et ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) ) )
7 anass 
 |-  ( ( ( ph /\ ps ) /\ et ) <-> ( ph /\ ( ps /\ et ) ) )
8 7 anbi1i 
 |-  ( ( ( ( ph /\ ps ) /\ et ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) <-> ( ( ph /\ ( ps /\ et ) ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) )
9 ancom 
 |-  ( ( ( ( ps /\ et ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) /\ ph ) <-> ( ph /\ ( ( ps /\ et ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) ) )
10 6 8 9 3bitr4ri 
 |-  ( ( ( ( ps /\ et ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) /\ ph ) <-> ( ( ( ph /\ ps ) /\ et ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) )
11 ancom 
 |-  ( ( ( ph /\ ps ) /\ et ) <-> ( et /\ ( ph /\ ps ) ) )
12 11 anbi1i 
 |-  ( ( ( ( ph /\ ps ) /\ et ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) <-> ( ( et /\ ( ph /\ ps ) ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) )
13 anass 
 |-  ( ( ( et /\ ( ph /\ ps ) ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) <-> ( et /\ ( ( ph /\ ps ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) ) )
14 ancom 
 |-  ( ( et /\ ( ( ph /\ ps ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) ) <-> ( ( ( ph /\ ps ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) /\ et ) )
15 13 14 bitri 
 |-  ( ( ( et /\ ( ph /\ ps ) ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) <-> ( ( ( ph /\ ps ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) /\ et ) )
16 10 12 15 3bitri 
 |-  ( ( ( ( ps /\ et ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) /\ ph ) <-> ( ( ( ph /\ ps ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) /\ et ) )
17 2 5 16 3bitr4ri 
 |-  ( ( ( ( ps /\ et ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) /\ ph ) <-> ( ( ( ph /\ ( ps /\ th ) ) /\ ( ch /\ ta ) ) /\ et ) )
18 anass 
 |-  ( ( ( ph /\ ( ps /\ th ) ) /\ ( ch /\ ta ) ) <-> ( ph /\ ( ( ps /\ th ) /\ ( ch /\ ta ) ) ) )
19 18 anbi1i 
 |-  ( ( ( ( ph /\ ( ps /\ th ) ) /\ ( ch /\ ta ) ) /\ et ) <-> ( ( ph /\ ( ( ps /\ th ) /\ ( ch /\ ta ) ) ) /\ et ) )
20 an4 
 |-  ( ( ( ps /\ th ) /\ ( ch /\ ta ) ) <-> ( ( ps /\ ch ) /\ ( th /\ ta ) ) )
21 anass 
 |-  ( ( ( ps /\ ch ) /\ ( th /\ ta ) ) <-> ( ps /\ ( ch /\ ( th /\ ta ) ) ) )
22 20 21 bitri 
 |-  ( ( ( ps /\ th ) /\ ( ch /\ ta ) ) <-> ( ps /\ ( ch /\ ( th /\ ta ) ) ) )
23 22 anbi2i 
 |-  ( ( ph /\ ( ( ps /\ th ) /\ ( ch /\ ta ) ) ) <-> ( ph /\ ( ps /\ ( ch /\ ( th /\ ta ) ) ) ) )
24 23 anbi1i 
 |-  ( ( ( ph /\ ( ( ps /\ th ) /\ ( ch /\ ta ) ) ) /\ et ) <-> ( ( ph /\ ( ps /\ ( ch /\ ( th /\ ta ) ) ) ) /\ et ) )
25 17 19 24 3bitri 
 |-  ( ( ( ( ps /\ et ) /\ ( ( ph /\ th ) /\ ( ch /\ ta ) ) ) /\ ph ) <-> ( ( ph /\ ( ps /\ ( ch /\ ( th /\ ta ) ) ) ) /\ et ) )