Metamath Proof Explorer

Theorem 3an4anass

Description: Associative law for four conjunctions with a triple conjunction. (Contributed by Alexander van der Vekens, 24-Jun-2018)

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

Step	Hyp	Ref	Expression
1		df-3an	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land χ)$
2	1	anbi1i	$⊢ ((φ \land ψ \land χ) \land θ) \leftrightarrow (((φ \land ψ) \land χ) \land θ)$
3		anass	$⊢ (((φ \land ψ) \land χ) \land θ) \leftrightarrow ((φ \land ψ) \land (χ \land θ))$
4	2 3	bitri	$⊢ ((φ \land ψ \land χ) \land θ) \leftrightarrow ((φ \land ψ) \land (χ \land θ))$