Metamath Proof Explorer

Theorem anandi3r

Description: Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018)

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

Step	Hyp	Ref	Expression
1		3anan32	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ \land χ) \land ψ)$
2		anandir	$⊢ ((φ \land χ) \land ψ) \leftrightarrow ((φ \land ψ) \land (χ \land ψ))$
3	1 2	bitri	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land (χ \land ψ))$