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

Theorem an33rean 1437
Description: Rearrange a 9-fold conjunction. (Contributed by Thierry Arnoux, 14-Apr-2019.)
Assertion
Ref Expression
an33rean (((𝜑𝜓𝜒) ∧ (𝜃𝜏𝜂) ∧ (𝜁𝜎𝜌)) ↔ ((𝜑𝜏𝜌) ∧ ((𝜓𝜃) ∧ (𝜂𝜎) ∧ (𝜒𝜁))))

Proof of Theorem an33rean
StepHypRef Expression
1 3anass 1034 . . 3 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
2 3anan12 1043 . . 3 ((𝜃𝜏𝜂) ↔ (𝜏 ∧ (𝜃𝜂)))
3 3anrev 1041 . . . 4 ((𝜁𝜎𝜌) ↔ (𝜌𝜎𝜁))
4 3anass 1034 . . . 4 ((𝜌𝜎𝜁) ↔ (𝜌 ∧ (𝜎𝜁)))
53, 4bitri 262 . . 3 ((𝜁𝜎𝜌) ↔ (𝜌 ∧ (𝜎𝜁)))
61, 2, 53anbi123i 1243 . 2 (((𝜑𝜓𝜒) ∧ (𝜃𝜏𝜂) ∧ (𝜁𝜎𝜌)) ↔ ((𝜑 ∧ (𝜓𝜒)) ∧ (𝜏 ∧ (𝜃𝜂)) ∧ (𝜌 ∧ (𝜎𝜁))))
7 3an6 1400 . 2 (((𝜑 ∧ (𝜓𝜒)) ∧ (𝜏 ∧ (𝜃𝜂)) ∧ (𝜌 ∧ (𝜎𝜁))) ↔ ((𝜑𝜏𝜌) ∧ ((𝜓𝜒) ∧ (𝜃𝜂) ∧ (𝜎𝜁))))
8 an4 860 . . . . . 6 (((𝜃𝜂) ∧ (𝜎𝜁)) ↔ ((𝜃𝜎) ∧ (𝜂𝜁)))
98anbi2i 725 . . . . 5 (((𝜓𝜒) ∧ ((𝜃𝜂) ∧ (𝜎𝜁))) ↔ ((𝜓𝜒) ∧ ((𝜃𝜎) ∧ (𝜂𝜁))))
10 3anass 1034 . . . . 5 (((𝜓𝜒) ∧ (𝜃𝜂) ∧ (𝜎𝜁)) ↔ ((𝜓𝜒) ∧ ((𝜃𝜂) ∧ (𝜎𝜁))))
11 3anass 1034 . . . . 5 (((𝜓𝜒) ∧ (𝜃𝜎) ∧ (𝜂𝜁)) ↔ ((𝜓𝜒) ∧ ((𝜃𝜎) ∧ (𝜂𝜁))))
129, 10, 113bitr4i 290 . . . 4 (((𝜓𝜒) ∧ (𝜃𝜂) ∧ (𝜎𝜁)) ↔ ((𝜓𝜒) ∧ (𝜃𝜎) ∧ (𝜂𝜁)))
13 an4 860 . . . . . 6 (((𝜓𝜒) ∧ (𝜃𝜎)) ↔ ((𝜓𝜃) ∧ (𝜒𝜎)))
1413anbi1i 726 . . . . 5 ((((𝜓𝜒) ∧ (𝜃𝜎)) ∧ (𝜂𝜁)) ↔ (((𝜓𝜃) ∧ (𝜒𝜎)) ∧ (𝜂𝜁)))
15 df-3an 1032 . . . . 5 (((𝜓𝜒) ∧ (𝜃𝜎) ∧ (𝜂𝜁)) ↔ (((𝜓𝜒) ∧ (𝜃𝜎)) ∧ (𝜂𝜁)))
16 df-3an 1032 . . . . 5 (((𝜓𝜃) ∧ (𝜒𝜎) ∧ (𝜂𝜁)) ↔ (((𝜓𝜃) ∧ (𝜒𝜎)) ∧ (𝜂𝜁)))
1714, 15, 163bitr4i 290 . . . 4 (((𝜓𝜒) ∧ (𝜃𝜎) ∧ (𝜂𝜁)) ↔ ((𝜓𝜃) ∧ (𝜒𝜎) ∧ (𝜂𝜁)))
18 3ancomb 1039 . . . . . 6 ((𝜓𝜒𝜂) ↔ (𝜓𝜂𝜒))
1918anbi1i 726 . . . . 5 (((𝜓𝜒𝜂) ∧ (𝜃𝜎𝜁)) ↔ ((𝜓𝜂𝜒) ∧ (𝜃𝜎𝜁)))
20 3an6 1400 . . . . 5 (((𝜓𝜃) ∧ (𝜒𝜎) ∧ (𝜂𝜁)) ↔ ((𝜓𝜒𝜂) ∧ (𝜃𝜎𝜁)))
21 3an6 1400 . . . . 5 (((𝜓𝜃) ∧ (𝜂𝜎) ∧ (𝜒𝜁)) ↔ ((𝜓𝜂𝜒) ∧ (𝜃𝜎𝜁)))
2219, 20, 213bitr4i 290 . . . 4 (((𝜓𝜃) ∧ (𝜒𝜎) ∧ (𝜂𝜁)) ↔ ((𝜓𝜃) ∧ (𝜂𝜎) ∧ (𝜒𝜁)))
2312, 17, 223bitri 284 . . 3 (((𝜓𝜒) ∧ (𝜃𝜂) ∧ (𝜎𝜁)) ↔ ((𝜓𝜃) ∧ (𝜂𝜎) ∧ (𝜒𝜁)))
2423anbi2i 725 . 2 (((𝜑𝜏𝜌) ∧ ((𝜓𝜒) ∧ (𝜃𝜂) ∧ (𝜎𝜁))) ↔ ((𝜑𝜏𝜌) ∧ ((𝜓𝜃) ∧ (𝜂𝜎) ∧ (𝜒𝜁))))
256, 7, 243bitri 284 1 (((𝜑𝜓𝜒) ∧ (𝜃𝜏𝜂) ∧ (𝜁𝜎𝜌)) ↔ ((𝜑𝜏𝜌) ∧ ((𝜓𝜃) ∧ (𝜂𝜎) ∧ (𝜒𝜁))))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  trgcgrg  25128
  Copyright terms: Public domain W3C validator