Metamath Proof Explorer

Theorem an31

Description: A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012) (Proof shortened by Wolf Lammen, 31-Dec-2012)

		Ref	Expression
	Assertion	an31	$⊢ ((φ \land ψ) \land χ) \leftrightarrow ((χ \land ψ) \land φ)$

Step	Hyp	Ref	Expression
1		an13	$⊢ (φ \land (ψ \land χ)) \leftrightarrow (χ \land (ψ \land φ))$
2		anass	$⊢ ((φ \land ψ) \land χ) \leftrightarrow (φ \land (ψ \land χ))$
3		anass	$⊢ ((χ \land ψ) \land φ) \leftrightarrow (χ \land (ψ \land φ))$
4	1 2 3	3bitr4i	$⊢ ((φ \land ψ) \land χ) \leftrightarrow ((χ \land ψ) \land φ)$