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

Metamath Proof Explorer