This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-3an

Description: Define conjunction ('and') of three wff's. Definition *4.34 of WhiteheadRussell p. 118. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law anass . (Contributed by NM, 8-Apr-1994)

		Ref	Expression
	Assertion	df-3an	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land χ)$

Detailed syntax breakdown

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