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	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	|- ph
1		wps	|- ps
2		wch	|- ch
3	0 1 2	w3a	|- ( ph /\ ps /\ ch )
4	0 1	wa	|- ( ph /\ ps )
5	4 2	wa	|- ( ( ph /\ ps ) /\ ch )
6	3 5	wb	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )