Definition df-3an 1089

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 468. (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 1087	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
5	1, 2	wa 395	. . 3 wff (𝜑 ∧ 𝜓)
6	5, 3	wa 395	. 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒)
7	4, 6	wb 206	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))

This definition is referenced by:  3anass  1095  3anan32  1097  3ancomb  1099  3anidm  1104  3an4anass  1105  3ioran  1106  3ianor  1107  3impa  1110  3expa  1119  3jca  1129  3anbi123i  1156  3pm3.2i  1341  3jaob  1429  3anbi123d  1439  3anim123d  1446  an6  1448  an3andi  1485  an33rean  1486  cadan  1611  19.26-3an  1874  nf3and  1900  nf3an  1903  4exdistr  1963  sb3an  2087  eeeanv  2355  mopick2  2638  r19.26-3  3098  r3al  3175  r3ex  3176  rexlimdvvva  3195  3reeanv  3210  ceqsex3v  3496  ceqsex4v  3497  ceqsex8v  3499  rspc4v  3597  sbc3an  3806  elin3  4159  rexdifpr  4617  raltpg  4656  tpss  4794  opthprneg  4822  dfopif  4827  disjxun  5097  otth2  5432  otthg  5434  oteqex  5449  poirr  5545  po3nr  5548  wefrc  5619  otelxp  5669  rabxp  5673  f1orn  6785  2f1fvneq  7208  fpropnf1  7215  dff1o6  7223  oprabidw  7391  oprabid  7392  oprabv  7420  ndmovass  7548  elovmpo  7605  elovmporab  7606  elovmporab1w  7607  elovmporab1  7608  elovmpt3rab1  7620  dfwe2  7721  opiota  8005  dfxp3  8007  bropopvvv  8034  poxp2  8087  xpord2pred  8089  xpord3pred  8096  sexp3  8097  oaord  8476  oeeu  8533  nnaord  8549  naddasslem1  8624  swoso  8672  fiint  9231  funsnfsupp  9299  ttrclselem2  9639  alephval3  10024  ingru  10730  axgroth3  10746  ltrelxr  11197  ltxrlt  11207  wloglei  11673  sup2  12102  rexuz2  12816  ltxr  13033  elixx3g  13278  ixxun  13281  dfrp2  13314  elioo4g  13326  elioopnf  13363  elioomnf  13364  elicopnf  13365  elxrge0  13377  divelunit  13414  elfz2  13434  elfzuzb  13438  uzsplit  13516  fznn0  13539  elfzmlbp  13559  preduz  13570  elfzo2  13582  fzolb2  13586  fzouzsplit  13614  ssfzo12bi  13681  fzind2  13708  hashgt23el  14351  ccatsymb  14510  swrdsbslen  14592  swrdspsleq  14593  swrdccatin2  14656  pfxccatin12lem2  14658  pfxccatin12lem3  14659  pfxccatin12  14660  pfxccat3a  14665  repsdf2  14705  repswsymball  14706  repswsymballbi  14707  repswswrd  14711  s3eq3seq  14866  wrdl3s3  14889  s3sndisj  14894  s3iunsndisj  14895  abs2dif  15260  sinltx  16118  divalglem8  16331  divalglem10  16333  divalgb  16335  bitsval2  16356  divgcdz  16442  rplpwr  16489  cncongr1  16598  pythagtriplem2  16749  pythagtrip  16766  prmgaplem4  16986  isstruct  17083  setsstruct2  17105  imasvscafn  17462  xpscf  17490  mreexmrid  17570  iscatd2  17608  issect  17681  issect2  17682  oppcsect  17706  isfunc  17792  funcpropd  17830  fucsect  17903  fucinv  17904  initoeu2  17944  setcsect  18017  setcinv  18018  issgrpd  18659  ismhm0  18719  issubm2  18733  issubg3  19078  resgrpisgrp  19081  eqgval  19110  eqger  19111  cycsubgcl  19139  isgim  19195  gim0to0  19202  gaorb  19240  gaorber  19241  gastacos  19243  symg2bas  19326  galactghm  19337  pmtr3ncom  19408  ispgp  19525  efgcpbllema  19687  efgcpbllemb  19688  eqgabl  19767  qusecsub  19768  cygabl  19824  dprdw  19945  omndmul2  20066  rnglz  20104  rngpropd  20113  ringpropd  20227  ringrghm  20252  isirred2  20361  rngcsect  20573  rngcinv  20574  ringcsect  20607  ringcinv  20608  drngid2  20689  issdrg2  20732  isorng  20798  islss  20889  islmim  21018  lmhmpropd  21029  zndvds  21508  znleval  21513  znleval2  21514  obselocv  21687  mpfrcl  22044  matinvgcell  22383  mat1dimscm  22423  scmatscm  22461  scmatf1  22479  mdetunilem7  22566  cpmatacl  22664  cpmatmcl  22667  mat2pmatf1  22677  mat2pmatghm  22678  mat2pmatmul  22679  mat2pmatlin  22683  mat2pmatscmxcl  22688  m2pmfzgsumcl  22696  decpmataa0  22716  monmatcollpw  22727  pmatcollpwscmatlem1  22737  pmatcollpwscmatlem2  22738  pm2mpghm  22764  pm2mpmhmlem2  22767  monmat2matmon  22772  chfacfisf  22802  chfacfisfcpmat  22803  chfacfpmmulgsum2  22813  isbasis3g  22897  leordtvallem2  23159  lmfval  23180  lmbr  23206  lmbr2  23207  lmmo  23328  dfconn2  23367  ptbasin  23525  ptbasfi  23529  txcnpi  23556  ptcnp  23570  hausdiag  23593  qtophmeo  23765  fbunfip  23817  elflim2  23912  hausflimi  23928  isfcls  23957  isfcls2  23961  istmd  24022  istgp  24025  istrg  24112  istdrg  24114  istdrg2  24126  istlm  24133  imasdsf1olem  24321  xmeterval  24380  xmeter  24381  prdsxmslem2  24477  blval2  24510  isngp  24544  isngp2  24545  isngp3  24546  isnlm  24623  cnbl0  24721  cnblcld  24722  elii1  24891  isphtpc  24953  phtpcer  24954  isclmp  25057  iscph  25130  lmmbr  25218  lmmbr2  25219  lmmbrf  25222  iscfil2  25226  iscau3  25238  iscau4  25239  iscauf  25240  caucfil  25243  isbn  25298  ishl2  25330  ovolfcl  25427  ioombl1lem4  25522  mbfmax  25610  iblpos  25754  limcrcl  25835  ig1pval3  26143  ulmdvlem3  26371  ellogdm  26608  relogbcl  26743  fsumvma2  27185  chpchtsum  27190  chpub  27191  dchrelbas3  27209  gausslemma2dlem1a  27336  noetalem1  27713  sltssnb  27769  eqcuts  27785  eqcuts2  27786  lnhl  28691  colopp  28845  dfcgra2  28906  axeuclidlem  29039  axeuclid  29040  edgupgr  29211  umgr2edg1  29288  subusgr  29366  nbgrel  29417  nb3grpr2  29460  nb3gr2nb  29461  isuvtx  29472  nbupgruvtxres  29484  iscplgredg  29494  cplgr3v  29512  rusgrpropedg  29662  rgrusgrprc  29667  rusgrprc  29668  upgriswlk  29718  wlkonprop  29734  wksonproplem  29780  usgr2pth0  29842  isclwlke  29854  crctcshtrl  29900  iswwlksnx  29917  wwlknbp  29919  2trld  30015  rusgrnumwwlkl1  30048  rusgrnumwwlkb0  30051  rusgrnumwwlk  30055  clwlkclwwlkflem  30083  erclwwlkref  30099  clwwlkwwlksb  30133  erclwwlknref  30148  clwwlknon2x  30182  0wlk  30195  3spthd  30255  umgr3v3e3cycl  30263  frgr3v  30354  1to3vfriswmgr  30359  frgr2wwlkeu  30406  numclwwlk1lem2fo  30437  dlwwlknondlwlknonf1o  30444  nvex  30690  isnv  30691  dfadj2  31964  cnvadj  31971  adjeq  32014  eleigvec  32036  eleigvec2  32037  chirredi  32473  or3di  32536  tpssg  32615  eliccelico  32859  pmtrprfv2  33172  fzto1st  33187  psgnfzto1st  33189  qusker  33432  qusxpid  33446  lsmsnorb  33474  prmidl0  33533  mxidlirred  33555  ply1degltel  33677  ply1degleel  33678  eulerpartlemv  34523  eulerpartlemd  34525  eulerpartlemn  34540  prob01  34572  probun  34578  bnj170  34856  bnj248  34858  bnj252  34861  bnj253  34862  bnj945  34931  bnj1098  34941  bnj1224  34959  bnj150  35034  bnj153  35038  bnj545  35053  bnj557  35059  bnj571  35064  bnj594  35070  bnj864  35080  bnj865  35081  bnj849  35083  bnj964  35101  bnj986  35113  bnj996  35114  bnj1033  35127  bnj1110  35140  bnj1128  35148  bnj1174  35161  subgrwlk  35328  cusgr3cyclex  35332  loop1cycl  35333  2cycl2d  35335  pconnconn  35427  resconn  35442  iscvm  35455  cvmlift2lem12  35510  cvmlift3lem5  35519  satfdm  35565  elmpst  35732  mpstrcl  35737  lediv2aALT  35873  3jcadALT  35883  dfso3  35916  br6  35953  elfuns  36109  brimg  36131  lemsuccf  36135  cgrxfr  36251  segcon2  36301  seglecgr12im  36306  seglecgr12  36307  segletr  36310  btwnoutside  36321  broutsideof3  36322  outsideoftr  36325  outsidele  36328  bj-imn3ani  36789  relowlpssretop  37571  wl-df3-3mintru2  37693  lindsenlbs  37818  matunitlindflem2  37820  fdc  37948  isbnd3b  37988  ablo4pnp  38083  crngm4  38206  isidlc  38218  pridl  38240  ispridl2  38241  ispridlc  38273  ts3an1  38353  ts3an2  38354  ts3an3  38355  brres2  38476  disjressuc2  38614  xrninxp  38618  dfsuccl4  38677  dfeqvrels2  38875  dfeqvrel2  38877  dfeqvrel3  38878  dfeldisj3  39014  islshpsm  39308  islshpat  39345  cmtfvalN  39538  cmtvalN  39539  ishlat1  39680  ishlat2  39681  3dim0  39785  2dim  39798  islvol5  39907  lhpexle3  40340  cdleme0ex2N  40552  cdleme0nex  40618  cdlemg2cex  40919  cdlemg33b0  41029  cdlemg33b  41035  cdlemg33c  41036  cdlemg33e  41038  dib1dim  41493  diblsmopel  41499  dihopelvalcpre  41576  lcfls1c  41864  aks6d1c1p1  42429  aks6d1c1p1rcl  42430  sn-sup2  42813  sn-isghm  42983  3anrabdioph  43091  fgraphxp  43513  omge2  43607  faosnf0.11b  43735  dfsucon  43831  pren2  43861  dfrtrcl5  43937  brfvrcld2  44000  df3an2  44077  dfvd3  44899  3impexpVD  45163  modelaxreplem1  45286  rfcnnnub  45348  stoweidlem35  46346  smflimlem4  47085  ndmaovass  47519  nltle2tri  47626  elfz2z  47628  prproropf1olem0  47815  reuprpr  47836  gboge9  48077  sbgoldbalt  48094  nnsum4primesodd  48109  nnsum4primesoddALTV  48110  bgoldbtbndlem4  48121  bgoldbtbnd  48122  dfvopnbgr2  48166  isuspgrim  48209  isubgr3stgrlem7  48285  grlimprop2  48299  uhgrimgrlim  48300  pgn4cyclex  48439  rngcsectALTV  48588  rngcinvALTV  48589  ringcsectALTV  48622  ringcinvALTV  48623  islindeps  48766  islindeps2  48796  isldepslvec2  48798  elbigo2  48865  line2ylem  49064  io1ii  49233  catprsc  49325  0funcglem  49395  0funclem  49398  catcsect  49710  isthincd2  49749  thincsect  49779  2arwcatlem1  49907