Definition df-3an 965

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 399. (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 963	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
5	1, 2	wa 103	. . 3 wff (𝜑 ∧ 𝜓)
6	5, 3	wa 103	. 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒)
7	4, 6	wb 104	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))

This definition is referenced by:  3anass  967  3anrot  968  3ancoma  970  3anan32  974  3ioran  978  3simpa  979  3pm3.2i  1160  pm3.2an3  1161  3jca  1162  3anbi123i  1171  3imp  1176  3anbi123d  1291  3anim123d  1298  an6  1300  19.26-3an  1460  hb3an  1530  nf3an  1546  nf3and  1549  eeeanv  1906  sb3an  1932  mopick2  2083  r19.26-3  2565  3reeanv  2604  ceqsex3v  2731  ceqsex4v  2732  ceqsex8v  2734  sbc3an  2974  elin3  3272  rexdifpr  3560  raltpg  3584  tpss  3693  dfopg  3711  opeq1  3713  opeq2  3714  opm  4164  otth2  4171  poirr  4237  po3nr  4240  wepo  4289  wetrep  4290  rabxp  4584  brinxp2  4614  brinxp  4615  sotri2  4944  sotri3  4945  f1orn  5385  dff1o6  5685  isosolem  5733  oprabid  5811  caovimo  5972  elovmpo  5979  dfxp3  6100  nnaord  6413  fiintim  6825  prmuloc  7398  ltrelxr  7849  rexuz2  9403  ltxr  9592  elixx3g  9714  elioo4g  9747  elioopnf  9780  elioomnf  9781  elicopnf  9782  elxrge0  9791  divelunit  9815  elfz2  9828  elfzuzb  9831  uzsplit  9903  fznn0  9924  elfzmlbp  9940  elfzo2  9958  fzolb2  9962  fzouzsplit  9987  ssfzo12bi  10033  fzind2  10047  abs2dif  10910  sumeq2  11160  divalgb  11658  divgcdz  11696  rplpwr  11751  cncongr1  11820  isbasis3g  12252  lmfval  12400  lmbr  12421  lmbr2  12422  xmeterval  12643  xmeter  12644  cnbl0  12742  cnblcld  12743  limcrcl  12835  bd3an  13199