This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem an33rean

Description: Rearrange a 9-fold conjunction. (Contributed by Thierry Arnoux, 14-Apr-2019) (Proof shortened by Wolf Lammen, 21-Apr-2024)

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

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 anass ⊢ ( ( ( 𝜃 ∧ 𝜂 ) ∧ 𝜎 ) ↔ ( 𝜃 ∧ ( 𝜂 ∧ 𝜎 ) ) )
9 8 anbi2i ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( ( 𝜃 ∧ 𝜂 ) ∧ 𝜎 ) ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ ( 𝜂 ∧ 𝜎 ) ) ) )
10 an42 ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ ( 𝜂 ∧ 𝜎 ) ) ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∧ ( ( 𝜂 ∧ 𝜎 ) ∧ 𝜒 ) ) )
11 9 10 bitri ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( ( 𝜃 ∧ 𝜂 ) ∧ 𝜎 ) ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∧ ( ( 𝜂 ∧ 𝜎 ) ∧ 𝜒 ) ) )
12 anass ⊢ ( ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜂 ) ) ∧ 𝜎 ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∧ ( ( 𝜃 ∧ 𝜂 ) ∧ 𝜎 ) ) )
13 anass ⊢ ( ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ) ∧ 𝜒 ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∧ ( ( 𝜂 ∧ 𝜎 ) ∧ 𝜒 ) ) )
14 11 12 13 3bitr4i ⊢ ( ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜂 ) ) ∧ 𝜎 ) ↔ ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ) ∧ 𝜒 ) )
15 14 anbi1i ⊢ ( ( ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜂 ) ) ∧ 𝜎 ) ∧ 𝜁 ) ↔ ( ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ) ∧ 𝜒 ) ∧ 𝜁 ) )
16 anass ⊢ ( ( ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜂 ) ) ∧ 𝜎 ) ∧ 𝜁 ) ↔ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜂 ) ) ∧ ( 𝜎 ∧ 𝜁 ) ) )
17 anass ⊢ ( ( ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ) ∧ 𝜒 ) ∧ 𝜁 ) ↔ ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ) ∧ ( 𝜒 ∧ 𝜁 ) ) )
18 15 16 17 3bitr3i ⊢ ( ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜂 ) ) ∧ ( 𝜎 ∧ 𝜁 ) ) ↔ ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ) ∧ ( 𝜒 ∧ 𝜁 ) ) )
19 df-3an ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜂 ) ∧ ( 𝜎 ∧ 𝜁 ) ) ↔ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜂 ) ) ∧ ( 𝜎 ∧ 𝜁 ) ) )
20 df-3an ⊢ ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ∧ ( 𝜒 ∧ 𝜁 ) ) ↔ ( ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ) ∧ ( 𝜒 ∧ 𝜁 ) ) )
21 18 19 20 3bitr4i ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜂 ) ∧ ( 𝜎 ∧ 𝜁 ) ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ∧ ( 𝜒 ∧ 𝜁 ) ) )
22 21 anbi2i ⊢ ( ( ( 𝜑 ∧ 𝜏 ∧ 𝜌 ) ∧ ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜂 ) ∧ ( 𝜎 ∧ 𝜁 ) ) ) ↔ ( ( 𝜑 ∧ 𝜏 ∧ 𝜌 ) ∧ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ∧ ( 𝜒 ∧ 𝜁 ) ) ) )
23 6 7 22 3bitri ⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜏 ∧ 𝜂 ) ∧ ( 𝜁 ∧ 𝜎 ∧ 𝜌 ) ) ↔ ( ( 𝜑 ∧ 𝜏 ∧ 𝜌 ) ∧ ( ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜂 ∧ 𝜎 ) ∧ ( 𝜒 ∧ 𝜁 ) ) ) )