Metamath Proof Explorer

Definition df-bnj17

Description: Define the 4-way conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-bnj17	$⊢ (φ \land ψ \land χ \land θ) \leftrightarrow ((φ \land ψ \land χ) \land θ)$

Step	Hyp	Ref	Expression
0		wph	$wff φ$
1		wps	$wff ψ$
2		wch	$wff χ$
3		wth	$wff θ$
4	0 1 2 3	w-bnj17	$wff (φ \land ψ \land χ \land θ)$
5	0 1 2	w3a	$wff (φ \land ψ \land χ)$
6	5 3	wa	$wff ((φ \land ψ \land χ) \land θ)$
7	4 6	wb	$wff ((φ \land ψ \land χ \land θ) \leftrightarrow ((φ \land ψ \land χ) \land θ))$