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