Metamath Proof Explorer

Theorem an33reanOLD

Description: Obsolete version of an33rean as of 21-Apr-2024. (Contributed by Thierry Arnoux, 14-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion an33reanOLD ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝜁 ∧ 𝜎 ∧ 𝜌 ) ) ↔ ( ( 𝜑 ∧ 𝜏 ∧ 𝜌 ) ∧ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ∧ ( 𝜒 ∧ 𝜁 ) ) ) )

Proof

Step Hyp Ref Expression
1 3anass ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) )
2 3anan12 ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜂 ) ↔ ( 𝜏 ∧ ( 𝜃 ∧ 𝜂 ) ) )
3 3anrev ⊢ ( ( 𝜁 ∧ 𝜎 ∧ 𝜌 ) ↔ ( 𝜌 ∧ 𝜎 ∧ 𝜁 ) )
4 3anass ⊢ ( ( 𝜌 ∧ 𝜎 ∧ 𝜁 ) ↔ ( 𝜌 ∧ ( 𝜎 ∧ 𝜁 ) ) )
5 3 4 bitri ⊢ ( ( 𝜁 ∧ 𝜎 ∧ 𝜌 ) ↔ ( 𝜌 ∧ ( 𝜎 ∧ 𝜁 ) ) )
6 1 2 5 3anbi123i ⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝜁 ∧ 𝜎 ∧ 𝜌 ) ) ↔ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) ∧ ( 𝜏 ∧ ( 𝜃 ∧ 𝜂 ) ) ∧ ( 𝜌 ∧ ( 𝜎 ∧ 𝜁 ) ) ) )
7 3an6 ⊢ ( ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) ∧ ( 𝜏 ∧ ( 𝜃 ∧ 𝜂 ) ) ∧ ( 𝜌 ∧ ( 𝜎 ∧ 𝜁 ) ) ) ↔ ( ( 𝜑 ∧ 𝜏 ∧ 𝜌 ) ∧ ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜂 ) ∧ ( 𝜎 ∧ 𝜁 ) ) ) )
8 an4 ⊢ ( ( ( 𝜃 ∧ 𝜂 ) ∧ ( 𝜎 ∧ 𝜁 ) ) ↔ ( ( 𝜃 ∧ 𝜎 ) ∧ ( 𝜂 ∧ 𝜁 ) ) )
9 8 anbi2i ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( ( 𝜃 ∧ 𝜂 ) ∧ ( 𝜎 ∧ 𝜁 ) ) ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∧ ( ( 𝜃 ∧ 𝜎 ) ∧ ( 𝜂 ∧ 𝜁 ) ) ) )
10 3anass ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜂 ) ∧ ( 𝜎 ∧ 𝜁 ) ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∧ ( ( 𝜃 ∧ 𝜂 ) ∧ ( 𝜎 ∧ 𝜁 ) ) ) )
11 3anass ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜎 ) ∧ ( 𝜂 ∧ 𝜁 ) ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∧ ( ( 𝜃 ∧ 𝜎 ) ∧ ( 𝜂 ∧ 𝜁 ) ) ) )
12 9 10 11 3bitr4i ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜂 ) ∧ ( 𝜎 ∧ 𝜁 ) ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜎 ) ∧ ( 𝜂 ∧ 𝜁 ) ) )
13 an4 ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜎 ) ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜎 ) ) )
14 13 anbi1i ⊢ ( ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜎 ) ) ∧ ( 𝜂 ∧ 𝜁 ) ) ↔ ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜎 ) ) ∧ ( 𝜂 ∧ 𝜁 ) ) )
15 df-3an ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜎 ) ∧ ( 𝜂 ∧ 𝜁 ) ) ↔ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜎 ) ) ∧ ( 𝜂 ∧ 𝜁 ) ) )
16 df-3an ⊢ ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜎 ) ∧ ( 𝜂 ∧ 𝜁 ) ) ↔ ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜎 ) ) ∧ ( 𝜂 ∧ 𝜁 ) ) )
17 14 15 16 3bitr4i ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜎 ) ∧ ( 𝜂 ∧ 𝜁 ) ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜎 ) ∧ ( 𝜂 ∧ 𝜁 ) ) )
18 3ancomb ⊢ ( ( 𝜓 ∧ 𝜒 ∧ 𝜂 ) ↔ ( 𝜓 ∧ 𝜂 ∧ 𝜒 ) )
19 18 anbi1i ⊢ ( ( ( 𝜓 ∧ 𝜒 ∧ 𝜂 ) ∧ ( 𝜃 ∧ 𝜎 ∧ 𝜁 ) ) ↔ ( ( 𝜓 ∧ 𝜂 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜎 ∧ 𝜁 ) ) )
20 3an6 ⊢ ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜎 ) ∧ ( 𝜂 ∧ 𝜁 ) ) ↔ ( ( 𝜓 ∧ 𝜒 ∧ 𝜂 ) ∧ ( 𝜃 ∧ 𝜎 ∧ 𝜁 ) ) )
21 3an6 ⊢ ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ∧ ( 𝜒 ∧ 𝜁 ) ) ↔ ( ( 𝜓 ∧ 𝜂 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜎 ∧ 𝜁 ) ) )
22 19 20 21 3bitr4i ⊢ ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜎 ) ∧ ( 𝜂 ∧ 𝜁 ) ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ∧ ( 𝜒 ∧ 𝜁 ) ) )
23 12 17 22 3bitri ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜂 ) ∧ ( 𝜎 ∧ 𝜁 ) ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ∧ ( 𝜒 ∧ 𝜁 ) ) )
24 23 anbi2i ⊢ ( ( ( 𝜑 ∧ 𝜏 ∧ 𝜌 ) ∧ ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜂 ) ∧ ( 𝜎 ∧ 𝜁 ) ) ) ↔ ( ( 𝜑 ∧ 𝜏 ∧ 𝜌 ) ∧ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ∧ ( 𝜒 ∧ 𝜁 ) ) ) )
25 6 7 24 3bitri ⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝜁 ∧ 𝜎 ∧ 𝜌 ) ) ↔ ( ( 𝜑 ∧ 𝜏 ∧ 𝜌 ) ∧ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ∧ ( 𝜒 ∧ 𝜁 ) ) ) )