Definition df-3an 929

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 394. (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 927	. 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  931  3anrot  932  3ancoma  934  3anan32  938  3ioran  942  3simpa  943  3pm3.2i  1124  pm3.2an3  1125  3jca  1126  3anbi123i  1135  3imp  1140  3anbi123d  1255  3anim123d  1262  an6  1264  19.26-3an  1424  hb3an  1494  nf3an  1510  nf3and  1513  eeeanv  1863  sb3an  1887  mopick2  2038  r19.26-3  2513  3reeanv  2551  ceqsex3v  2675  ceqsex4v  2676  ceqsex8v  2678  sbc3an  2914  elin3  3206  raltpg  3515  tpss  3624  dfopg  3642  opeq1  3644  opeq2  3645  opm  4085  otth2  4092  poirr  4158  po3nr  4161  wepo  4210  wetrep  4211  rabxp  4504  brinxp2  4534  brinxp  4535  sotri2  4862  sotri3  4863  f1orn  5298  dff1o6  5593  isosolem  5641  oprabid  5719  caovimo  5876  elovmpt2  5883  dfxp3  6002  nnaord  6308  fiintim  6719  prmuloc  7222  ltrelxr  7644  rexuz2  9168  ltxr  9345  elixx3g  9467  elioo4g  9500  elioopnf  9533  elioomnf  9534  elicopnf  9535  elxrge0  9544  divelunit  9568  elfz2  9580  elfzuzb  9583  uzsplit  9655  fznn0  9676  elfzmlbp  9692  elfzo2  9710  fzolb2  9714  fzouzsplit  9739  ssfzo12bi  9785  fzind2  9799  abs2dif  10654  sumeq2  10902  divalgb  11352  divgcdz  11390  rplpwr  11443  cncongr1  11512  isbasis3g  11896  lmfval  12044  lmbr  12064  lmbr2  12065  xmeterval  12221  xmeter  12222  cnbl0  12311  cnblcld  12312  bd3an  12429