Definition df-3an 1070

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 461. (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 1068	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
5	1, 2	wa 387	. . 3 wff (𝜑 ∧ 𝜓)
6	5, 3	wa 387	. 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒)
7	4, 6	wb 198	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))

This definition is referenced by:  3anass  1076  3anan32  1078  3ancomb  1080  3an4anass  1085  3ioran  1086  3ianor  1087  3impa  1090  3expa  1098  3jca  1108  3anbi123i  1135  3pm3.2i  1319  3anbi123d  1415  3anim123d  1422  an6  1424  an3andi  1461  an33rean  1462  cadan  1572  19.26-3an  1835  nf3and  1861  nf3an  1864  4exdistr  1921  sb3an  2032  eeeanv  2284  mopick2  2668  r19.26-3  3122  r3al  3152  3reeanv  3309  ceqsex3v  3466  ceqsex4v  3467  ceqsex8v  3469  sbc3an  3741  elin3  4065  rexdifpr  4470  raltpg  4508  tpss  4642  opthprneg  4669  dfopif  4674  disjxun  4927  otth2  5232  otthg  5234  oteqex  5246  poirr  5337  po3nr  5340  wefrc  5401  rabxp  5452  f1orn  6454  fpropnf1  6850  dff1o6  6857  oprabid  7007  oprabv  7033  ndmovass  7152  elovmpo  7209  elovmporab  7210  elovmporab1  7211  elovmpt3rab1  7223  dfwe2  7312  opiota  7565  dfxp3  7567  bropopvvv  7593  oaord  7974  oeeu  8030  nnaord  8046  swoso  8122  fiint  8590  funsnfsupp  8652  alephval3  9330  ingru  10035  axgroth3  10051  ltrelxr  10502  ltxrlt  10511  wloglei  10973  sup2  11398  rexuz2  12113  ltxr  12327  elixx3g  12567  ixxun  12570  elioo4g  12613  elioopnf  12647  elioomnf  12648  elicopnf  12649  elxrge0  12661  divelunit  12696  elfz2  12715  elfzuzb  12718  uzsplit  12795  fznn0  12815  elfzmlbp  12834  preduz  12845  elfzo2  12857  fzolb2  12861  fzouzsplit  12887  ssfzo12bi  12947  fzind2  12970  hashgt23el  13598  ccatsymb  13745  swrdsbslen  13841  swrdspsleq  13842  swrdccatin2  13929  pfxccatin12lem2  13931  swrdccatin12lem2OLD  13932  swrdccatin12lem3  13933  pfxccatin12  13934  swrdccatin12OLD  13935  pfxccat3a  13942  repsdf2  13997  repswsymball  13998  repswsymballbi  13999  repswswrd  14003  s3eq3seq  14163  wrdl3s3  14187  s3sndisj  14188  s3iunsndisj  14189  abs2dif  14553  sinltx  15402  divalglem8  15611  divalglem10  15613  divalgb  15615  bitsval2  15634  divgcdz  15720  rplpwr  15763  cncongr1  15867  pythagtriplem2  16010  pythagtrip  16027  prmgaplem4  16246  isstruct  16352  setsstruct2  16377  imasvscafn  16666  mreexmrid  16772  iscatd2  16810  issect  16881  issect2  16882  oppcsect  16906  isfunc  16992  funcpropd  17028  fucsect  17100  fucinv  17101  initoeu2  17134  setcsect  17207  setcinv  17208  issubm2  17816  issubg3  18081  resgrpisgrp  18084  cycsubgcl  18089  eqgval  18112  eqger  18113  isgim  18173  gaorb  18208  gaorber  18209  gastacos  18211  symg2bas  18287  galactghm  18292  gsmsymgreqlem2  18320  pmtr3ncom  18364  ispgp  18478  efgcpbllema  18640  efgcpbllemb  18641  eqgabl  18713  dprdw  18882  ringpropd  19055  ringrghm  19078  isirred2  19174  gim0to0  19218  rim0to0OLD  19219  drngid2  19241  issdrg2  19299  islss  19428  islmim  19556  lmhmpropd  19567  isassa  19809  mpfrcl  20011  zndvds  20398  znleval  20403  znleval2  20404  obselocv  20574  matinvgcell  20748  mat1dimscm  20788  scmatscm  20826  scmatf1  20844  mdetunilem7  20931  cpmatacl  21028  cpmatmcl  21031  mat2pmatf1  21041  mat2pmatghm  21042  mat2pmatmul  21043  mat2pmatlin  21047  mat2pmatscmxcl  21052  m2pmfzgsumcl  21060  decpmataa0  21080  monmatcollpw  21091  pmatcollpwscmatlem1  21101  pmatcollpwscmatlem2  21102  pm2mpghm  21128  pm2mpmhmlem2  21131  monmat2matmon  21136  chfacfisf  21166  chfacfisfcpmat  21167  chfacfpmmulgsum2  21177  isbasis3g  21261  leordtvallem2  21523  lmfval  21544  lmbr  21570  lmbr2  21571  lmmo  21692  dfconn2  21731  ptbasin  21889  ptbasfi  21893  txcnpi  21920  ptcnp  21934  hausdiag  21957  qtophmeo  22129  fbunfip  22181  elflim2  22276  hausflimi  22292  isfcls  22321  isfcls2  22325  istmd  22386  istgp  22389  istrg  22475  istdrg  22477  istdrg2  22489  istlm  22496  imasdsf1olem  22686  xmeterval  22745  xmeter  22746  prdsxmslem2  22842  blval2  22875  isngp  22908  isngp2  22909  isngp3  22910  isnlm  22987  cnbl0  23085  cnblcld  23086  elii1  23242  isphtpc  23301  phtpcer  23302  isclmp  23404  iscph  23477  lmmbr  23564  lmmbr2  23565  lmmbrf  23568  iscfil2  23572  iscau3  23584  iscau4  23585  iscauf  23586  caucfil  23589  isbn  23644  ishl2  23676  ovolfcl  23770  ioombl1lem4  23865  mbfmax  23953  iblpos  24096  limcrcl  24175  ig1pval3  24471  ulmdvlem3  24693  ellogdm  24923  relogbcl  25052  fsumvma2  25492  chpchtsum  25497  chpub  25498  dchrelbas3  25516  gausslemma2dlem1a  25643  lnhl  26103  colopp  26257  dfcgra2  26318  axeuclidlem  26451  axeuclid  26452  edgupgr  26622  umgr2edg1  26696  subusgr  26774  nbgrel  26825  nb3grpr2  26868  nb3gr2nb  26869  isuvtx  26880  nbupgruvtxres  26892  iscplgredg  26902  cplgr3v  26920  rusgrpropedg  27069  rgrusgrprc  27074  rusgrprc  27075  upgriswlk  27125  wlkonprop  27142  wksonproplem  27194  usgr2pth0  27254  isclwlke  27266  crctcshtrl  27309  iswwlksnx  27326  wwlknbp  27328  2trld  27444  rusgrnumwwlkl1  27474  rusgrnumwwlkb0  27477  rusgrnumwwlk  27482  clwlkclwwlkflem  27512  erclwwlkref  27535  clwwlkwwlksb  27577  erclwwlknref  27593  clwwlknon2x  27631  0wlk  27645  3spthd  27705  umgr3v3e3cycl  27713  frgr3v  27809  1to3vfriswmgr  27814  frgr2wwlkeu  27861  numclwwlk1lem2fo  27900  numclwwlk1lem2foOLD  27905  dlwwlknondlwlknonf1o  27916  dlwwlknondlwlknonf1oOLD  27917  nvex  28165  isnv  28166  dfadj2  29443  cnvadj  29450  adjeq  29493  eleigvec  29515  eleigvec2  29516  chirredi  29952  or3di  30006  dfrp2  30250  eliccelico  30259  omndmul2  30437  isorng  30557  qusker  30603  pmtrprfv2  30695  fzto1st  30700  psgnfzto1st  30702  eulerpartlemv  31273  eulerpartlemd  31275  eulerpartlemn  31290  prob01  31323  probun  31329  bnj170  31622  bnj248  31624  bnj252  31627  bnj253  31628  bnj945  31699  bnj1098  31709  bnj1224  31727  bnj150  31801  bnj153  31805  bnj545  31820  bnj557  31826  bnj571  31831  bnj594  31837  bnj864  31847  bnj865  31848  bnj849  31850  bnj964  31868  bnj986  31879  bnj996  31880  bnj1033  31892  bnj1110  31905  bnj1128  31913  bnj1174  31926  pconnconn  32069  resconn  32084  iscvm  32097  cvmlift2lem12  32152  cvmlift3lem5  32161  elmpst  32309  mpstrcl  32314  lediv2aALT  32446  dfso3  32476  br6  32519  etasslt  32801  elfuns  32903  brimg  32925  brsuccf  32929  cgrxfr  33043  segcon2  33093  seglecgr12im  33098  seglecgr12  33099  segletr  33102  btwnoutside  33113  broutsideof3  33114  outsideoftr  33117  outsidele  33120  bj-imn3ani  33444  relowlpssretop  34093  lindsenlbs  34334  matunitlindflem2  34336  fdc  34468  isbnd3b  34511  ablo4pnp  34606  crngm4  34729  isidlc  34741  pridl  34763  ispridl2  34764  ispridlc  34796  ts3an1  34878  ts3an2  34879  ts3an3  34880  brres2  34979  xrninxp  35091  dfeqvrels2  35274  dfeqvrel2  35276  dfeqvrel3  35277  dfeldisj3  35403  islshpsm  35567  islshpat  35604  cmtfvalN  35797  cmtvalN  35798  ishlat1  35939  ishlat2  35940  3dim0  36044  2dim  36057  islvol5  36166  lhpexle3  36599  cdleme0ex2N  36811  cdleme0nex  36877  cdlemg2cex  37178  cdlemg33b0  37288  cdlemg33b  37294  cdlemg33c  37295  cdlemg33e  37297  dib1dim  37752  diblsmopel  37758  dihopelvalcpre  37835  lcfls1c  38123  3anrabdioph  38781  fgraphxp  39213  dfrtrcl5  39358  brfvrcld2  39406  df3an2  39483  dfvd3  40350  3impexpVD  40615  rfcnnnub  40718  stoweidlem35  41757  smflimlem4  42487  ndmaovass  42817  nltle2tri  42925  elfz2z  42927  prproropf1olem0  43038  reuprpr  43059  gboge9  43303  sbgoldbalt  43320  nnsum4primesodd  43335  nnsum4primesoddALTV  43336  bgoldbtbndlem4  43347  bgoldbtbnd  43348  ismhm0  43446  rnglz  43525  rngcsect  43621  rngcinv  43622  rngcsectALTV  43633  rngcinvALTV  43634  ringcsect  43672  ringcinv  43673  ringcsectALTV  43696  ringcinvALTV  43697  islindeps  43881  islindeps2  43911  isldepslvec2  43913  elbigo2  43986  line2ylem  44112