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

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

Proof of Theorem an33rean
StepHypRef Expression
1 3anass 977 . . 3
2 3anan12 986 . . 3
3 3anrev 984 . . . 4
4 3anass 977 . . . 4
53, 4bitri 249 . . 3
61, 2, 53anbi123i 1185 . 2
7 3an6 1309 . 2
8 an4 824 . . . . . 6
98anbi2i 694 . . . . 5
10 3anass 977 . . . . 5
11 3anass 977 . . . . 5
129, 10, 113bitr4i 277 . . . 4
13 an4 824 . . . . . 6
1413anbi1i 695 . . . . 5
15 df-3an 975 . . . . 5
16 df-3an 975 . . . . 5
1714, 15, 163bitr4i 277 . . . 4
18 3ancomb 982 . . . . . 6
1918anbi1i 695 . . . . 5
20 3an6 1309 . . . . 5
21 3an6 1309 . . . . 5
2219, 20, 213bitr4i 277 . . . 4
2312, 17, 223bitri 271 . . 3
2423anbi2i 694 . 2
256, 7, 243bitri 271 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  /\wa 369  /\w3a 973 This theorem is referenced by:  trgcgrg  23906 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 975
 Copyright terms: Public domain W3C validator