13an22anass

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

		Ref	Expression
	Assertion	13an22anass	$⊢ (φ \land (ψ \land χ \land θ)) \leftrightarrow ((φ \land ψ) \land (χ \land θ))$

Step	Hyp	Ref	Expression
1		an2anr	$⊢ ((ψ \land χ) \land (θ \land φ)) \leftrightarrow ((χ \land ψ) \land (φ \land θ))$
2		an2anr	$⊢ ((φ \land χ) \land (θ \land ψ)) \leftrightarrow ((χ \land φ) \land (ψ \land θ))$
3		an4	$⊢ ((χ \land φ) \land (ψ \land θ)) \leftrightarrow ((χ \land ψ) \land (φ \land θ))$
4	2 3	bitri	$⊢ ((φ \land χ) \land (θ \land ψ)) \leftrightarrow ((χ \land ψ) \land (φ \land θ))$
5		an43	$⊢ ((φ \land χ) \land (θ \land ψ)) \leftrightarrow ((φ \land ψ) \land (χ \land θ))$
6	1 4 5	3bitr2ri	$⊢ ((φ \land ψ) \land (χ \land θ)) \leftrightarrow ((ψ \land χ) \land (θ \land φ))$
7		3an4anass	$⊢ ((ψ \land χ \land θ) \land φ) \leftrightarrow ((ψ \land χ) \land (θ \land φ))$
8		ancom	$⊢ ((ψ \land χ \land θ) \land φ) \leftrightarrow (φ \land (ψ \land χ \land θ))$
9	6 7 8	3bitr2ri	$⊢ (φ \land (ψ \land χ \land θ)) \leftrightarrow ((φ \land ψ) \land (χ \land θ))$

Metamath Proof Explorer