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	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2		wch	⊢ 𝜒
3	0 1 2	w3a	⊢ ( 𝜑 ∧ 𝜓 ∧ 𝜒 )
4	0 1	wa	⊢ ( 𝜑 ∧ 𝜓 )
5	4 2	wa	⊢ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 )
6	3 5	wb	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )