Definition df-3an 1101

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

This definition is referenced by:  3anass  1107  3anan32OLD  1110  3ancomb  1112  3anidm  1117  3an4anass  1118  3ioran  1119  3ianor  1120  3impa  1123  3expa  1132  3jca  1142  3anbi123i  1169  3pm3.2i  1354  3jaob  1447  3anbi123d  1459  3anim123d  1466  an6  1468  an3andi  1505  an33rean  1506  cadan  1631  19.26-3an  1894  nf3and  1920  nf3an  1923  4exdistr  1983  sb3an  2116  eeeanv  2383  mopick2  2666  r19.26-3  3125  r3al  3202  r3ex  3203  rexlimdvvva  3222  3reeanv  3237  ceqsex3v  3508  ceqsex4v  3509  ceqsex8v  3511  rspc4v  3603  sbc3an  3810  elin3  4160  rexdifpr  4620  raltpg  4659  tpss  4797  opthprneg  4825  dfopif  4830  disjxun  5100  otth2  5453  otthg  5455  oteqex  5471  poirr  5569  po3nr  5572  wefrc  5643  otelxp  5693  rabxp  5697  f1orn  6819  2f1fvneq  7246  fpropnf1  7253  dff1o6  7261  oprabidw  7429  oprabid  7430  oprabv  7458  ndmovass  7586  elovmpo  7643  elovmporab  7644  elovmporab1w  7645  elovmporab1  7646  elovmpt3rab1  7658  dfwe2  7759  opiota  8042  dfxp3  8044  bropopvvv  8071  poxp2  8125  xpord2pred  8127  xpord3pred  8134  sexp3  8135  oaord  8518  oeeu  8575  nnaord  8591  naddasslem1  8667  swoso  8715  fiint  9273  funsnfsupp  9340  ttrclselem2  9683  alephval3  10068  ingru  10775  axgroth3  10791  ltrelxr  11245  ltxrlt  11255  wloglei  11721  sup2  12150  rexuz2  12902  ltxr  13119  elixx3g  13364  ixxun  13367  dfrp2  13400  elioo4g  13412  elioopnf  13449  elioomnf  13450  elicopnf  13451  elxrge0  13463  divelunit  13500  elfz2  13521  elfzuzb  13525  uzsplit  13603  fznn0  13626  elfzmlbp  13646  preduz  13657  elfzo2  13669  fzolb2  13674  fzouzsplit  13702  ssfzo12bi  13769  fzind2  13796  hashgt23el  14439  ccatsymb  14598  swrdsbslen  14680  swrdspsleq  14681  swrdccatin2  14744  pfxccatin12lem2  14746  pfxccatin12lem3  14747  pfxccatin12  14748  pfxccat3a  14753  repsdf2  14793  repswsymball  14794  repswsymballbi  14795  repswswrd  14799  s3eq3seq  14954  wrdl3s3  14977  s3sndisj  14982  s3iunsndisj  14983  abs2dif  15362  sinltx  16223  divalglem8  16436  divalglem10  16438  divalgb  16440  bitsval2  16461  divgcdz  16547  rplpwr  16594  cncongr1  16703  pythagtriplem2  16855  pythagtrip  16872  prmgaplem4  17092  isstruct  17190  setsstruct2  17212  imasvscafn  17569  xpscf  17597  mreexmrid  17677  iscatd2  17715  issect  17788  issect2  17789  oppcsect  17813  isfunc  17899  funcpropd  17937  fucsect  18010  fucinv  18011  initoeu2  18051  setcsect  18124  setcinv  18125  issgrpd  18766  ismhm0  18826  issubm2  18840  issubg3  19188  resgrpisgrp  19191  eqgval  19220  eqger  19221  cycsubgcl  19249  isgim  19304  gim0to0  19311  gaorb  19349  gaorber  19350  gastacos  19352  symg2bas  19435  galactghm  19446  pmtr3ncom  19517  ispgp  19634  efgcpbllema  19796  efgcpbllemb  19797  eqgabl  19876  qusecsub  19877  cygabl  19933  dprdw  20054  omndmul2  20175  rnglz  20213  rngpropd  20222  ringpropd  20340  ringrghm  20365  isirred2  20472  rngcsect  20688  rngcinv  20689  ringcsect  20722  ringcinv  20723  drngid2  20804  issdrg2  20846  isorng  20912  islss  21003  islmim  21131  lmhmpropd  21142  zndvds  21603  znleval  21608  znleval2  21609  obselocv  21782  mpfrcl  22140  matinvgcell  22497  mat1dimscm  22537  scmatscm  22575  scmatf1  22593  mdetunilem7  22680  cpmatacl  22778  cpmatmcl  22781  mat2pmatf1  22791  mat2pmatghm  22792  mat2pmatmul  22793  mat2pmatlin  22797  mat2pmatscmxcl  22802  m2pmfzgsumcl  22810  decpmataa0  22830  monmatcollpw  22841  pmatcollpwscmatlem1  22851  pmatcollpwscmatlem2  22852  pm2mpghm  22878  pm2mpmhmlem2  22881  monmat2matmon  22886  chfacfisf  22916  chfacfisfcpmat  22917  chfacfpmmulgsum2  22927  isbasis3g  23011  leordtvallem2  23273  lmfval  23294  lmbr  23320  lmbr2  23321  lmmo  23442  dfconn2  23481  ptbasin  23639  ptbasfi  23643  txcnpi  23670  ptcnp  23684  hausdiag  23707  qtophmeo  23879  fbunfip  23931  elflim2  24026  hausflimi  24042  isfcls  24071  isfcls2  24075  istmd  24136  istgp  24139  istrg  24226  istdrg  24228  istdrg2  24240  istlm  24247  imasdsf1olem  24435  xmeterval  24494  xmeter  24495  prdsxmslem2  24591  blval2  24624  isngp  24658  isngp2  24659  isngp3  24660  isnlm  24737  cnbl0  24835  cnblcld  24836  elii1  24999  isphtpc  25058  phtpcer  25059  isclmp  25161  iscph  25234  lmmbr  25322  lmmbr2  25323  lmmbrf  25326  iscfil2  25330  iscau3  25342  iscau4  25343  iscauf  25344  caucfil  25347  isbn  25402  ishl2  25434  ovolfcl  25530  ioombl1lem4  25625  mbfmax  25713  iblpos  25857  limcrcl  25938  ig1pval3  26240  ulmdvlem3  26467  ellogdm  26706  relogbcl  26840  fsumvma2  27280  chpchtsum  27285  chpub  27286  dchrelbas3  27304  gausslemma2dlem1a  27431  noetalem1  27807  sltssnb  27864  eqcuts  27880  eqcuts2  27881  lnhl  28786  colopp  28944  dfcgra2  29026  axeuclidlem  29165  axeuclid  29166  edgupgr  29337  umgr2edg1  29414  subusgr  29492  nbgrel  29543  nb3grpr2  29586  nb3gr2nb  29587  isuvtx  29598  nbupgruvtxres  29610  iscplgredg  29620  cplgr3v  29638  rusgrpropedg  29787  rgrusgrprc  29792  rusgrprc  29793  upgriswlk  29843  wlkonprop  29859  wksonproplem  29905  usgr2pth0  29967  isclwlke  29979  crctcshtrl  30025  iswwlksnx  30042  wwlknbp  30044  2trld  30140  rusgrnumwwlkl1  30173  rusgrnumwwlkb0  30176  rusgrnumwwlk  30180  clwlkclwwlkflem  30208  erclwwlkref  30224  clwwlkwwlksb  30258  erclwwlknref  30273  clwwlknon2x  30307  0wlk  30320  3spthd  30380  umgr3v3e3cycl  30388  frgr3v  30479  1to3vfriswmgr  30484  frgr2wwlkeu  30531  numclwwlk1lem2fo  30562  dlwwlknondlwlknonf1o  30569  nvex  30816  isnv  30817  dfadj2  32090  cnvadj  32097  adjeq  32140  eleigvec  32162  eleigvec2  32163  chirredi  32599  or3di  32661  tpssg  32738  eliccelico  32981  pmtrprfv2  33270  fzto1st  33285  psgnfzto1st  33287  qusker  33537  qusxpid  33551  lsmsnorb  33579  prmidl0  33639  mxidlirred  33662  ply1degltel  33792  ply1degleel  33793  eulerpartlemv  34663  eulerpartlemd  34665  eulerpartlemn  34680  prob01  34712  probun  34718  bnj170  34996  bnj248  34998  bnj252  35001  bnj253  35002  bnj945  35071  bnj1098  35081  bnj1224  35098  bnj150  35173  bnj153  35177  bnj545  35192  bnj557  35198  bnj571  35203  bnj594  35209  bnj864  35219  bnj865  35220  bnj849  35222  bnj964  35240  bnj986  35252  bnj996  35253  bnj1033  35266  bnj1110  35279  bnj1128  35287  bnj1174  35300  subgrwlk  35487  cusgr3cyclex  35491  loop1cycl  35492  2cycl2d  35494  pconnconn  35586  resconn  35601  iscvm  35614  cvmlift2lem12  35669  cvmlift3lem5  35678  satfdm  35724  elmpst  35891  mpstrcl  35896  lediv2aALT  36032  3jcadALT  36042  dfso3  36075  br6  36112  elfuns  36268  brimg  36290  lemsuccf  36294  cgrxfr  36410  segcon2  36460  seglecgr12im  36465  seglecgr12  36466  segletr  36469  btwnoutside  36480  broutsideof3  36481  outsideoftr  36484  outsidele  36487  bj-imn3ani  37035  relowlpssretop  37863  wl-df3-3mintru2  37985  lindsenlbs  38119  matunitlindflem2  38121  fdc  38249  isbnd3b  38289  ablo4pnp  38384  crngm4  38507  isidlc  38519  pridl  38541  ispridl2  38542  ispridlc  38574  ts3an1  38654  ts3an2  38655  ts3an3  38656  brres2  38777  disjressuc2  38915  xrninxp  38919  dfsuccl4  38978  dfeqvrels2  39176  dfeqvrel2  39178  dfeqvrel3  39179  dfeldisj3  39315  islshpsm  39609  islshpat  39646  cmtfvalN  39839  cmtvalN  39840  ishlat1  39981  ishlat2  39982  3dim0  40086  2dim  40099  islvol5  40208  lhpexle3  40641  cdleme0ex2N  40853  cdleme0nex  40919  cdlemg2cex  41220  cdlemg33b0  41330  cdlemg33b  41336  cdlemg33c  41337  cdlemg33e  41339  dib1dim  41794  diblsmopel  41800  dihopelvalcpre  41877  lcfls1c  42165  aks6d1c1p1  42729  aks6d1c1p1rcl  42730  sn-sup2  43118  sn-isghm  43260  3anrabdioph  43368  fgraphxp  43786  omge2  43880  faosnf0.11b  44008  dfsucon  44104  pren2  44134  dfrtrcl5  44210  brfvrcld2  44273  df3an2  44350  dfvd3  45172  3impexpVD  45436  modelaxreplem1  45559  rfcnnnub  45621  stoweidlem35  46614  smflimlem4  47353  ndmaovass  47805  nltle2tri  47912  elfz2z  47914  prproropf1olem0  48113  reuprpr  48134  gboge9  48391  sbgoldbalt  48408  nnsum4primesodd  48423  nnsum4primesoddALTV  48424  bgoldbtbndlem4  48435  bgoldbtbnd  48436  dfvopnbgr2  48480  isuspgrim  48523  isubgr3stgrlem7  48599  grlimprop2  48613  uhgrimgrlim  48614  pgn4cyclex  48753  rngcsectALTV  48902  rngcinvALTV  48903  ringcsectALTV  48936  ringcinvALTV  48937  islindeps  49080  islindeps2  49110  isldepslvec2  49112  elbigo2  49179  line2ylem  49378  io1ii  49547  catprsc  49639  0funcglem  49709  0funclem  49712  catcsect  50024  isthincd2  50063  thincsect  50093  2arwcatlem1  50221