anan

Description: Multiple commutations in conjunction. (Contributed by Peter Mazsa, 7-Mar-2020)

		Ref	Expression
	Assertion	anan	$⊢ (((φ \land ψ) \land χ) \land ((φ \land θ) \land τ)) \leftrightarrow ((ψ \land θ) \land (φ \land (χ \land τ)))$

Step	Hyp	Ref	Expression
1		an4	$⊢ (((φ \land ψ) \land χ) \land ((φ \land θ) \land τ)) \leftrightarrow (((φ \land ψ) \land (φ \land θ)) \land (χ \land τ))$
2		anandi	$⊢ (φ \land (ψ \land θ)) \leftrightarrow ((φ \land ψ) \land (φ \land θ))$
3		ancom	$⊢ (φ \land (ψ \land θ)) \leftrightarrow ((ψ \land θ) \land φ)$
4	2 3	bitr3i	$⊢ ((φ \land ψ) \land (φ \land θ)) \leftrightarrow ((ψ \land θ) \land φ)$
5	4	anbi1i	$⊢ (((φ \land ψ) \land (φ \land θ)) \land (χ \land τ)) \leftrightarrow (((ψ \land θ) \land φ) \land (χ \land τ))$
6		anass	$⊢ (((ψ \land θ) \land φ) \land (χ \land τ)) \leftrightarrow ((ψ \land θ) \land (φ \land (χ \land τ)))$
7	1 5 6	3bitri	$⊢ (((φ \land ψ) \land χ) \land ((φ \land θ) \land τ)) \leftrightarrow ((ψ \land θ) \land (φ \land (χ \land τ)))$

Metamath Proof Explorer