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 ( ( 𝜑 ∧ ( 𝜓𝜒𝜃 ) ) ↔ ( ( 𝜑𝜓 ) ∧ ( 𝜒𝜃 ) ) )