Metamath Proof Explorer

Theorem 3an6

Description: Analogue of an4 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011) (Proof shortened by Andrew Salmon, 25-May-2011)

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

Step	Hyp	Ref	Expression
1		an6	$⊢ ((φ \land χ \land τ) \land (ψ \land θ \land η)) \leftrightarrow ((φ \land ψ) \land (χ \land θ) \land (τ \land η))$
2	1	bicomi	$⊢ ((φ \land ψ) \land (χ \land θ) \land (τ \land η)) \leftrightarrow ((φ \land χ \land τ) \land (ψ \land θ \land η))$