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

Metamath Proof Explorer

Theorem 13an22anass

Description: Associative law for four conjunctions with a triple conjunction. (Contributed by Thierry Arnoux, 21-Jan-2025)

Ref Expression
Assertion 13an22anass ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) )

Proof

Step Hyp Ref Expression
1 an2anr ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜑 ) ) ↔ ( ( 𝜒 ∧ 𝜓 ) ∧ ( 𝜑 ∧ 𝜃 ) ) )
2 an2anr ⊢ ( ( ( 𝜑 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜓 ) ) ↔ ( ( 𝜒 ∧ 𝜑 ) ∧ ( 𝜓 ∧ 𝜃 ) ) )
3 an4 ⊢ ( ( ( 𝜒 ∧ 𝜑 ) ∧ ( 𝜓 ∧ 𝜃 ) ) ↔ ( ( 𝜒 ∧ 𝜓 ) ∧ ( 𝜑 ∧ 𝜃 ) ) )
4 2 3 bitri ⊢ ( ( ( 𝜑 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜓 ) ) ↔ ( ( 𝜒 ∧ 𝜓 ) ∧ ( 𝜑 ∧ 𝜃 ) ) )
5 an43 ⊢ ( ( ( 𝜑 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜓 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) )
6 1 4 5 3bitr2ri ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜑 ) ) )
7 3an4anass ⊢ ( ( ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ∧ 𝜑 ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∧ ( 𝜃 ∧ 𝜑 ) ) )
8 ancom ⊢ ( ( ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ∧ 𝜑 ) ↔ ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ) )
9 6 7 8 3bitr2ri ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) )