an6

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

Step	Hyp	Ref	Expression
1		an4	$⊢ (((φ \land ψ) \land χ) \land ((θ \land τ) \land η)) \leftrightarrow (((φ \land ψ) \land (θ \land τ)) \land (χ \land η))$
2		an4	$⊢ ((φ \land ψ) \land (θ \land τ)) \leftrightarrow ((φ \land θ) \land (ψ \land τ))$
3	1 2	bianbi	$⊢ (((φ \land ψ) \land χ) \land ((θ \land τ) \land η)) \leftrightarrow (((φ \land θ) \land (ψ \land τ)) \land (χ \land η))$
4		df-3an	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land χ)$
5		df-3an	$⊢ (θ \land τ \land η) \leftrightarrow ((θ \land τ) \land η)$
6	4 5	anbi12i	$⊢ ((φ \land ψ \land χ) \land (θ \land τ \land η)) \leftrightarrow (((φ \land ψ) \land χ) \land ((θ \land τ) \land η))$
7		df-3an	$⊢ ((φ \land θ) \land (ψ \land τ) \land (χ \land η)) \leftrightarrow (((φ \land θ) \land (ψ \land τ)) \land (χ \land η))$
8	3 6 7	3bitr4i	$⊢ ((φ \land ψ \land χ) \land (θ \land τ \land η)) \leftrightarrow ((φ \land θ) \land (ψ \land τ) \land (χ \land η))$

Metamath Proof Explorer