Definition df-3an 873

Description: Define conjunction ('and') of 3 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 383. (Contributed by NM, 8-Apr-1994.)

Assertion

Ref	Expression
df-3an	⊢ ((φ ∧ ψ ∧ χ) ↔ ((φ ∧ ψ) ∧ χ))

Detailed syntax breakdown of Definition df-3an

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		wps	. . 3 wff ψ
3		wch	. . 3 wff χ
4	1, 2, 3	w3a 871	. 2 wff (φ ∧ ψ ∧ χ)
5	1, 2	wa 97	. . 3 wff (φ ∧ ψ)
6	5, 3	wa 97	. 2 wff ((φ ∧ ψ) ∧ χ)
7	4, 6	wb 98	1 wff ((φ ∧ ψ ∧ χ) ↔ ((φ ∧ ψ) ∧ χ))

This definition is referenced by:  3anass  875  3anrot  876  3ancoma  878  3anan32  882  3ioran  886  3simpa  887  3pm3.2i  1065  pm3.2an3  1066  3jca  1067  3anbi123i  1077  3imp  1082  3anbi123d  1190  3anim123d  1197  an6  1199  19.26-3an  1348  hb3an  1420  nf3an  1436  nf3and  1439  eeeanv  1786  sb3an  1810  mopick2  1961  r19.26-3  2417  3reeanv  2454  ceqsex3v  2569  ceqsex4v  2570  ceqsex8v  2572  elin3  3101  raltpg  3393  tpss  3499  dfopg  3517  opeq1  3519  opeq2  3520  opm  3941  otth2  3948  poirr  4014  po3nr  4017  rabxp  4303  brinxp2  4330  brinxp  4331  sotri2  4645  sotri3  4646  f1orn  5057  dff1o6  5337  isosolem  5384  oprabid  5457  caovimo  5613  elovmpt2  5620  dfxp3  5739  nnaord  5989  prmuloc  6404  ltrelxr  6675  bd3an  7196