an3andi

Description: Distribution of conjunction over threefold conjunction. (Contributed by Thierry Arnoux, 8-Apr-2019)

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

Step	Hyp	Ref	Expression
1		anandi	$⊢ (φ \land ((ψ \land χ) \land θ)) \leftrightarrow ((φ \land (ψ \land χ)) \land (φ \land θ))$
2		anandi	$⊢ (φ \land (ψ \land χ)) \leftrightarrow ((φ \land ψ) \land (φ \land χ))$
3	1 2	bianbi	$⊢ (φ \land ((ψ \land χ) \land θ)) \leftrightarrow (((φ \land ψ) \land (φ \land χ)) \land (φ \land θ))$
4		df-3an	$⊢ (ψ \land χ \land θ) \leftrightarrow ((ψ \land χ) \land θ)$
5	4	anbi2i	$⊢ (φ \land (ψ \land χ \land θ)) \leftrightarrow (φ \land ((ψ \land χ) \land θ))$
6		df-3an	$⊢ ((φ \land ψ) \land (φ \land χ) \land (φ \land θ)) \leftrightarrow (((φ \land ψ) \land (φ \land χ)) \land (φ \land θ))$
7	3 5 6	3bitr4i	$⊢ (φ \land (ψ \land χ \land θ)) \leftrightarrow ((φ \land ψ) \land (φ \land χ) \land (φ \land θ))$

Metamath Proof Explorer