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

Metamath Proof Explorer

Theorem an6

Description: Rearrangement of 6 conjuncts. (Contributed by NM, 13-Mar-1995)

Ref Expression
Assertion an6 ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜏 ∧ 𝜂 ) ) ↔ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜓 ∧ 𝜏 ) ∧ ( 𝜒 ∧ 𝜂 ) ) )

Proof

Step Hyp Ref Expression
1 an4 ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ ( ( 𝜃 ∧ 𝜏 ) ∧ 𝜂 ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜃 ∧ 𝜏 ) ) ∧ ( 𝜒 ∧ 𝜂 ) ) )
2 an4 ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜃 ∧ 𝜏 ) ) ↔ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜓 ∧ 𝜏 ) ) )
3 1 2 bianbi ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ ( ( 𝜃 ∧ 𝜏 ) ∧ 𝜂 ) ) ↔ ( ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜓 ∧ 𝜏 ) ) ∧ ( 𝜒 ∧ 𝜂 ) ) )
4 df-3an ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )
5 df-3an ⊢ ( ( 𝜃 ∧ 𝜏 ∧ 𝜂 ) ↔ ( ( 𝜃 ∧ 𝜏 ) ∧ 𝜂 ) )
6 4 5 anbi12i ⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜏 ∧ 𝜂 ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ ( ( 𝜃 ∧ 𝜏 ) ∧ 𝜂 ) ) )
7 df-3an ⊢ ( ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜓 ∧ 𝜏 ) ∧ ( 𝜒 ∧ 𝜂 ) ) ↔ ( ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜓 ∧ 𝜏 ) ) ∧ ( 𝜒 ∧ 𝜂 ) ) )
8 3 6 7 3bitr4i ⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜏 ∧ 𝜂 ) ) ↔ ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜓 ∧ 𝜏 ) ∧ ( 𝜒 ∧ 𝜂 ) ) )