Metamath Proof Explorer

Theorem 13an22anassOLD

Description: Obsolete version of 13an22anass as of 31-Oct-2026. (Contributed by Thierry Arnoux, 21-Jan-2025) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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 θ))$