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

Theorem an33reanOLD 1481
Description: Obsolete version of an33rean 1480 as of 21-Apr-2024. (Contributed by Thierry Arnoux, 14-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
an33reanOLD (((𝜑𝜓𝜒) ∧ (𝜃𝜏𝜂) ∧ (𝜁𝜎𝜌)) ↔ ((𝜑𝜏𝜌) ∧ ((𝜓𝜃) ∧ (𝜂𝜎) ∧ (𝜒𝜁))))

Proof of Theorem an33reanOLD
StepHypRef Expression
1 3anass 1092 . . 3 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
2 3anan12 1093 . . 3 ((𝜃𝜏𝜂) ↔ (𝜏 ∧ (𝜃𝜂)))
3 3anrev 1098 . . . 4 ((𝜁𝜎𝜌) ↔ (𝜌𝜎𝜁))
4 3anass 1092 . . . 4 ((𝜌𝜎𝜁) ↔ (𝜌 ∧ (𝜎𝜁)))
53, 4bitri 278 . . 3 ((𝜁𝜎𝜌) ↔ (𝜌 ∧ (𝜎𝜁)))
61, 2, 53anbi123i 1152 . 2 (((𝜑𝜓𝜒) ∧ (𝜃𝜏𝜂) ∧ (𝜁𝜎𝜌)) ↔ ((𝜑 ∧ (𝜓𝜒)) ∧ (𝜏 ∧ (𝜃𝜂)) ∧ (𝜌 ∧ (𝜎𝜁))))
7 3an6 1443 . 2 (((𝜑 ∧ (𝜓𝜒)) ∧ (𝜏 ∧ (𝜃𝜂)) ∧ (𝜌 ∧ (𝜎𝜁))) ↔ ((𝜑𝜏𝜌) ∧ ((𝜓𝜒) ∧ (𝜃𝜂) ∧ (𝜎𝜁))))
8 an4 655 . . . . . 6 (((𝜃𝜂) ∧ (𝜎𝜁)) ↔ ((𝜃𝜎) ∧ (𝜂𝜁)))
98anbi2i 625 . . . . 5 (((𝜓𝜒) ∧ ((𝜃𝜂) ∧ (𝜎𝜁))) ↔ ((𝜓𝜒) ∧ ((𝜃𝜎) ∧ (𝜂𝜁))))
10 3anass 1092 . . . . 5 (((𝜓𝜒) ∧ (𝜃𝜂) ∧ (𝜎𝜁)) ↔ ((𝜓𝜒) ∧ ((𝜃𝜂) ∧ (𝜎𝜁))))
11 3anass 1092 . . . . 5 (((𝜓𝜒) ∧ (𝜃𝜎) ∧ (𝜂𝜁)) ↔ ((𝜓𝜒) ∧ ((𝜃𝜎) ∧ (𝜂𝜁))))
129, 10, 113bitr4i 306 . . . 4 (((𝜓𝜒) ∧ (𝜃𝜂) ∧ (𝜎𝜁)) ↔ ((𝜓𝜒) ∧ (𝜃𝜎) ∧ (𝜂𝜁)))
13 an4 655 . . . . . 6 (((𝜓𝜒) ∧ (𝜃𝜎)) ↔ ((𝜓𝜃) ∧ (𝜒𝜎)))
1413anbi1i 626 . . . . 5 ((((𝜓𝜒) ∧ (𝜃𝜎)) ∧ (𝜂𝜁)) ↔ (((𝜓𝜃) ∧ (𝜒𝜎)) ∧ (𝜂𝜁)))
15 df-3an 1086 . . . . 5 (((𝜓𝜒) ∧ (𝜃𝜎) ∧ (𝜂𝜁)) ↔ (((𝜓𝜒) ∧ (𝜃𝜎)) ∧ (𝜂𝜁)))
16 df-3an 1086 . . . . 5 (((𝜓𝜃) ∧ (𝜒𝜎) ∧ (𝜂𝜁)) ↔ (((𝜓𝜃) ∧ (𝜒𝜎)) ∧ (𝜂𝜁)))
1714, 15, 163bitr4i 306 . . . 4 (((𝜓𝜒) ∧ (𝜃𝜎) ∧ (𝜂𝜁)) ↔ ((𝜓𝜃) ∧ (𝜒𝜎) ∧ (𝜂𝜁)))
18 3ancomb 1096 . . . . . 6 ((𝜓𝜒𝜂) ↔ (𝜓𝜂𝜒))
1918anbi1i 626 . . . . 5 (((𝜓𝜒𝜂) ∧ (𝜃𝜎𝜁)) ↔ ((𝜓𝜂𝜒) ∧ (𝜃𝜎𝜁)))
20 3an6 1443 . . . . 5 (((𝜓𝜃) ∧ (𝜒𝜎) ∧ (𝜂𝜁)) ↔ ((𝜓𝜒𝜂) ∧ (𝜃𝜎𝜁)))
21 3an6 1443 . . . . 5 (((𝜓𝜃) ∧ (𝜂𝜎) ∧ (𝜒𝜁)) ↔ ((𝜓𝜂𝜒) ∧ (𝜃𝜎𝜁)))
2219, 20, 213bitr4i 306 . . . 4 (((𝜓𝜃) ∧ (𝜒𝜎) ∧ (𝜂𝜁)) ↔ ((𝜓𝜃) ∧ (𝜂𝜎) ∧ (𝜒𝜁)))
2312, 17, 223bitri 300 . . 3 (((𝜓𝜒) ∧ (𝜃𝜂) ∧ (𝜎𝜁)) ↔ ((𝜓𝜃) ∧ (𝜂𝜎) ∧ (𝜒𝜁)))
2423anbi2i 625 . 2 (((𝜑𝜏𝜌) ∧ ((𝜓𝜒) ∧ (𝜃𝜂) ∧ (𝜎𝜁))) ↔ ((𝜑𝜏𝜌) ∧ ((𝜓𝜃) ∧ (𝜂𝜎) ∧ (𝜒𝜁))))
256, 7, 243bitri 300 1 (((𝜑𝜓𝜒) ∧ (𝜃𝜏𝜂) ∧ (𝜁𝜎𝜌)) ↔ ((𝜑𝜏𝜌) ∧ ((𝜓𝜃) ∧ (𝜂𝜎) ∧ (𝜒𝜁))))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator