Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  an33rean Structured version   Unicode version

Theorem an33rean 1333
 Description: Rearrange 9-fold conjunction. (Contributed by Thierry Arnoux, 14-Apr-2019.)
Assertion
Ref Expression
an33rean

Proof of Theorem an33rean
StepHypRef Expression
1 3anass 969 . . 3
2 3anrot 970 . . . 4
3 3ancomb 974 . . . 4
4 3anass 969 . . . 4
52, 3, 43bitri 271 . . 3
6 3anrev 976 . . . 4
7 3anass 969 . . . 4
86, 7bitri 249 . . 3
91, 5, 83anbi123i 1177 . 2
10 3an6 1300 . 2
11 an4 820 . . . . . 6
1211anbi2i 694 . . . . 5
13 3anass 969 . . . . 5
14 3anass 969 . . . . 5
1512, 13, 143bitr4i 277 . . . 4
16 an4 820 . . . . . 6
1716anbi1i 695 . . . . 5
18 df-3an 967 . . . . 5
19 df-3an 967 . . . . 5
2017, 18, 193bitr4i 277 . . . 4
21 3ancomb 974 . . . . . 6
2221anbi1i 695 . . . . 5
23 3an6 1300 . . . . 5
24 3an6 1300 . . . . 5
2522, 23, 243bitr4i 277 . . . 4
2615, 20, 253bitri 271 . . 3
2726anbi2i 694 . 2
289, 10, 273bitri 271 1
 Colors of variables: wff setvar class Syntax hints:   wb 184   wa 369   w3a 965 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967 This theorem is referenced by:  trgcgrg  23104
 Copyright terms: Public domain W3C validator