Definition df-3an 975

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 973	. 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  977  3anrot  978  3ancoma  980  3anan32  984  3ioran  988  3simpa  989  3pm3.2i  1170  pm3.2an3  1171  3jca  1172  3anbi123i  1183  3imp  1188  3anbi123d  1307  3anim123d  1314  an6  1316  19.26-3an  1476  hb3an  1543  nf3an  1559  nf3and  1562  eeeanv  1926  sb3an  1951  mopick2  2102  r19.26-3  2600  3reeanv  2640  ceqsex3v  2772  ceqsex4v  2773  ceqsex8v  2775  sbc3an  3016  elin3  3318  rexdifpr  3611  raltpg  3636  tpss  3745  dfopg  3763  opeq1  3765  opeq2  3766  opm  4219  otth2  4226  poirr  4292  po3nr  4295  wepo  4344  wetrep  4345  rabxp  4648  brinxp2  4678  brinxp  4679  sotri2  5008  sotri3  5009  f1orn  5452  dff1o6  5755  isosolem  5803  oprabid  5885  caovimo  6046  elovmpo  6050  dfxp3  6173  nnaord  6488  fiintim  6906  prmuloc  7528  ltrelxr  7980  rexuz2  9540  ltxr  9732  elixx3g  9858  elioo4g  9891  elioopnf  9924  elioomnf  9925  elicopnf  9926  elxrge0  9935  divelunit  9959  elfz2  9972  elfzuzb  9975  uzsplit  10048  fznn0  10069  elfzmlbp  10088  elfzo2  10106  fzolb2  10110  fzouzsplit  10135  ssfzo12bi  10181  fzind2  10195  dfrp2  10220  abs2dif  11070  sumeq2  11322  divalgb  11884  divgcdz  11926  rplpwr  11982  nnwosdc  11994  cncongr1  12057  pythagtriplem2  12220  pythagtrip  12237  isbasis3g  12838  lmfval  12986  lmbr  13007  lmbr2  13008  xmeterval  13229  xmeter  13230  cnbl0  13328  cnblcld  13329  limcrcl  13421  bd3an  13865