Definition df-3an 1088

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 1086	. 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  1094  3anan32  1096  3ancomb  1098  3anidm  1103  3an4anass  1104  3ioran  1105  3ianor  1106  3impa  1109  3expa  1118  3jca  1128  3anbi123i  1155  3pm3.2i  1340  3jaob  1428  3anbi123d  1438  3anim123d  1445  an6  1447  an3andi  1484  an33rean  1485  cadan  1609  19.26-3an  1872  nf3and  1898  nf3an  1901  4exdistr  1961  sb3an  2082  eeeanv  2348  mopick2  2630  r19.26-3  3090  r3al  3167  r3ex  3168  rexlimdvvva  3187  3reeanv  3202  ceqsex3v  3494  ceqsex4v  3495  ceqsex8v  3497  rspc4v  3599  sbc3an  3809  elin3  4159  rexdifpr  4613  raltpg  4652  tpss  4791  opthprneg  4819  dfopif  4824  disjxun  5093  otth2  5430  otthg  5432  oteqex  5447  poirr  5543  po3nr  5546  wefrc  5617  otelxp  5667  rabxp  5671  f1orn  6778  2f1fvneq  7201  fpropnf1  7208  dff1o6  7216  oprabidw  7384  oprabid  7385  oprabv  7413  ndmovass  7541  elovmpo  7598  elovmporab  7599  elovmporab1w  7600  elovmporab1  7601  elovmpt3rab1  7613  dfwe2  7714  opiota  8001  dfxp3  8003  bropopvvv  8030  poxp2  8083  xpord2pred  8085  xpord3pred  8092  sexp3  8093  oaord  8472  oeeu  8528  nnaord  8544  naddasslem1  8619  swoso  8666  fiint  9235  fiintOLD  9236  funsnfsupp  9301  ttrclselem2  9641  alephval3  10023  ingru  10728  axgroth3  10744  ltrelxr  11195  ltxrlt  11204  wloglei  11670  sup2  12099  rexuz2  12818  ltxr  13035  elixx3g  13279  ixxun  13282  dfrp2  13315  elioo4g  13327  elioopnf  13364  elioomnf  13365  elicopnf  13366  elxrge0  13378  divelunit  13415  elfz2  13435  elfzuzb  13439  uzsplit  13517  fznn0  13540  elfzmlbp  13560  preduz  13571  elfzo2  13583  fzolb2  13587  fzouzsplit  13615  ssfzo12bi  13682  fzind2  13706  hashgt23el  14349  ccatsymb  14507  swrdsbslen  14589  swrdspsleq  14590  swrdccatin2  14653  pfxccatin12lem2  14655  pfxccatin12lem3  14656  pfxccatin12  14657  pfxccat3a  14662  repsdf2  14702  repswsymball  14703  repswsymballbi  14704  repswswrd  14708  s3eq3seq  14864  wrdl3s3  14887  s3sndisj  14892  s3iunsndisj  14893  abs2dif  15258  sinltx  16116  divalglem8  16329  divalglem10  16331  divalgb  16333  bitsval2  16354  divgcdz  16440  rplpwr  16487  cncongr1  16596  pythagtriplem2  16747  pythagtrip  16764  prmgaplem4  16984  isstruct  17081  setsstruct2  17103  imasvscafn  17459  xpscf  17487  mreexmrid  17567  iscatd2  17605  issect  17678  issect2  17679  oppcsect  17703  isfunc  17789  funcpropd  17827  fucsect  17900  fucinv  17901  initoeu2  17941  setcsect  18014  setcinv  18015  issgrpd  18622  ismhm0  18682  issubm2  18696  issubg3  19041  resgrpisgrp  19044  eqgval  19074  eqger  19075  cycsubgcl  19103  isgim  19159  gim0to0  19166  gaorb  19204  gaorber  19205  gastacos  19207  symg2bas  19290  galactghm  19301  pmtr3ncom  19372  ispgp  19489  efgcpbllema  19651  efgcpbllemb  19652  eqgabl  19731  qusecsub  19732  cygabl  19788  dprdw  19909  omndmul2  20030  rnglz  20068  rngpropd  20077  ringpropd  20191  ringrghm  20216  isirred2  20324  rngcsect  20539  rngcinv  20540  ringcsect  20573  ringcinv  20574  drngid2  20655  issdrg2  20698  isorng  20764  islss  20855  islmim  20984  lmhmpropd  20995  zndvds  21474  znleval  21479  znleval2  21480  obselocv  21653  mpfrcl  22008  matinvgcell  22338  mat1dimscm  22378  scmatscm  22416  scmatf1  22434  mdetunilem7  22521  cpmatacl  22619  cpmatmcl  22622  mat2pmatf1  22632  mat2pmatghm  22633  mat2pmatmul  22634  mat2pmatlin  22638  mat2pmatscmxcl  22643  m2pmfzgsumcl  22651  decpmataa0  22671  monmatcollpw  22682  pmatcollpwscmatlem1  22692  pmatcollpwscmatlem2  22693  pm2mpghm  22719  pm2mpmhmlem2  22722  monmat2matmon  22727  chfacfisf  22757  chfacfisfcpmat  22758  chfacfpmmulgsum2  22768  isbasis3g  22852  leordtvallem2  23114  lmfval  23135  lmbr  23161  lmbr2  23162  lmmo  23283  dfconn2  23322  ptbasin  23480  ptbasfi  23484  txcnpi  23511  ptcnp  23525  hausdiag  23548  qtophmeo  23720  fbunfip  23772  elflim2  23867  hausflimi  23883  isfcls  23912  isfcls2  23916  istmd  23977  istgp  23980  istrg  24067  istdrg  24069  istdrg2  24081  istlm  24088  imasdsf1olem  24277  xmeterval  24336  xmeter  24337  prdsxmslem2  24433  blval2  24466  isngp  24500  isngp2  24501  isngp3  24502  isnlm  24579  cnbl0  24677  cnblcld  24678  elii1  24847  isphtpc  24909  phtpcer  24910  isclmp  25013  iscph  25086  lmmbr  25174  lmmbr2  25175  lmmbrf  25178  iscfil2  25182  iscau3  25194  iscau4  25195  iscauf  25196  caucfil  25199  isbn  25254  ishl2  25286  ovolfcl  25383  ioombl1lem4  25478  mbfmax  25566  iblpos  25710  limcrcl  25791  ig1pval3  26099  ulmdvlem3  26327  ellogdm  26564  relogbcl  26699  fsumvma2  27141  chpchtsum  27146  chpub  27147  dchrelbas3  27165  gausslemma2dlem1a  27292  noetalem1  27669  eqscut  27734  eqscut2  27735  lnhl  28578  colopp  28732  dfcgra2  28793  axeuclidlem  28925  axeuclid  28926  edgupgr  29097  umgr2edg1  29174  subusgr  29252  nbgrel  29303  nb3grpr2  29346  nb3gr2nb  29347  isuvtx  29358  nbupgruvtxres  29370  iscplgredg  29380  cplgr3v  29398  rusgrpropedg  29548  rgrusgrprc  29553  rusgrprc  29554  upgriswlk  29604  wlkonprop  29620  wksonproplem  29666  usgr2pth0  29728  isclwlke  29740  crctcshtrl  29786  iswwlksnx  29803  wwlknbp  29805  2trld  29901  rusgrnumwwlkl1  29931  rusgrnumwwlkb0  29934  rusgrnumwwlk  29938  clwlkclwwlkflem  29966  erclwwlkref  29982  clwwlkwwlksb  30016  erclwwlknref  30031  clwwlknon2x  30065  0wlk  30078  3spthd  30138  umgr3v3e3cycl  30146  frgr3v  30237  1to3vfriswmgr  30242  frgr2wwlkeu  30289  numclwwlk1lem2fo  30320  dlwwlknondlwlknonf1o  30327  nvex  30573  isnv  30574  dfadj2  31847  cnvadj  31854  adjeq  31897  eleigvec  31919  eleigvec2  31920  chirredi  32356  or3di  32421  tpssg  32499  eliccelico  32733  pmtrprfv2  33043  fzto1st  33058  psgnfzto1st  33060  qusker  33296  qusxpid  33310  lsmsnorb  33338  prmidl0  33397  mxidlirred  33419  ply1degltel  33536  ply1degleel  33537  eulerpartlemv  34331  eulerpartlemd  34333  eulerpartlemn  34348  prob01  34380  probun  34386  bnj170  34664  bnj248  34666  bnj252  34669  bnj253  34670  bnj945  34739  bnj1098  34749  bnj1224  34767  bnj150  34842  bnj153  34846  bnj545  34861  bnj557  34867  bnj571  34872  bnj594  34878  bnj864  34888  bnj865  34889  bnj849  34891  bnj964  34909  bnj986  34921  bnj996  34922  bnj1033  34935  bnj1110  34948  bnj1128  34956  bnj1174  34969  subgrwlk  35104  cusgr3cyclex  35108  loop1cycl  35109  2cycl2d  35111  pconnconn  35203  resconn  35218  iscvm  35231  cvmlift2lem12  35286  cvmlift3lem5  35295  satfdm  35341  elmpst  35508  mpstrcl  35513  lediv2aALT  35649  3jcadALT  35659  dfso3  35692  br6  35729  elfuns  35888  brimg  35910  brsuccf  35914  cgrxfr  36028  segcon2  36078  seglecgr12im  36083  seglecgr12  36084  segletr  36087  btwnoutside  36098  broutsideof3  36099  outsideoftr  36102  outsidele  36105  bj-imn3ani  36560  relowlpssretop  37337  wl-df3-3mintru2  37459  lindsenlbs  37594  matunitlindflem2  37596  fdc  37724  isbnd3b  37764  ablo4pnp  37859  crngm4  37982  isidlc  37994  pridl  38016  ispridl2  38017  ispridlc  38049  ts3an1  38129  ts3an2  38130  ts3an3  38131  brres2  38242  disjressuc2  38359  xrninxp  38363  dfeqvrels2  38564  dfeqvrel2  38566  dfeqvrel3  38567  dfeldisj3  38696  islshpsm  38958  islshpat  38995  cmtfvalN  39188  cmtvalN  39189  ishlat1  39330  ishlat2  39331  3dim0  39436  2dim  39449  islvol5  39558  lhpexle3  39991  cdleme0ex2N  40203  cdleme0nex  40269  cdlemg2cex  40570  cdlemg33b0  40680  cdlemg33b  40686  cdlemg33c  40687  cdlemg33e  40689  dib1dim  41144  diblsmopel  41150  dihopelvalcpre  41227  lcfls1c  41515  aks6d1c1p1  42080  aks6d1c1p1rcl  42081  sn-sup2  42464  sn-isghm  42646  3anrabdioph  42755  fgraphxp  43177  omge2  43271  faosnf0.11b  43400  dfsucon  43496  pren2  43526  dfrtrcl5  43602  brfvrcld2  43665  df3an2  43742  dfvd3  44565  3impexpVD  44829  modelaxreplem1  44952  rfcnnnub  45014  stoweidlem35  46017  smflimlem4  46756  ndmaovass  47191  nltle2tri  47298  elfz2z  47300  prproropf1olem0  47487  reuprpr  47508  gboge9  47749  sbgoldbalt  47766  nnsum4primesodd  47781  nnsum4primesoddALTV  47782  bgoldbtbndlem4  47793  bgoldbtbnd  47794  dfvopnbgr2  47838  isuspgrim  47881  isubgr3stgrlem7  47957  grlimprop2  47971  uhgrimgrlim  47972  pgn4cyclex  48111  rngcsectALTV  48260  rngcinvALTV  48261  ringcsectALTV  48294  ringcinvALTV  48295  islindeps  48439  islindeps2  48469  isldepslvec2  48471  elbigo2  48538  line2ylem  48737  io1ii  48906  catprsc  48999  0funcglem  49069  0funclem  49072  catcsect  49384  isthincd2  49423  thincsect  49453  2arwcatlem1  49581