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	2	anbi1i	$⊢ (((φ \land ψ) \land (θ \land τ)) \land (χ \land η)) \leftrightarrow (((φ \land θ) \land (ψ \land τ)) \land (χ \land η))$
4	1 3	bitri	$⊢ (((φ \land ψ) \land χ) \land ((θ \land τ) \land η)) \leftrightarrow (((φ \land θ) \land (ψ \land τ)) \land (χ \land η))$
5		df-3an	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land χ)$
6		df-3an	$⊢ (θ \land τ \land η) \leftrightarrow ((θ \land τ) \land η)$
7	5 6	anbi12i	$⊢ ((φ \land ψ \land χ) \land (θ \land τ \land η)) \leftrightarrow (((φ \land ψ) \land χ) \land ((θ \land τ) \land η))$
8		df-3an	$⊢ ((φ \land θ) \land (ψ \land τ) \land (χ \land η)) \leftrightarrow (((φ \land θ) \land (ψ \land τ)) \land (χ \land η))$
9	4 7 8	3bitr4i	$⊢ ((φ \land ψ \land χ) \land (θ \land τ \land η)) \leftrightarrow ((φ \land θ) \land (ψ \land τ) \land (χ \land η))$

Metamath Proof Explorer