Definition df-3an 1105

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 474. (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 1103	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
5	1, 2	wa 401	. . 3 wff (𝜑 ∧ 𝜓)
6	5, 3	wa 401	. 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒)
7	4, 6	wb 209	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))

This definition is used by:  3anass  1111  3anan32OLD  1114  3ancomb  1116  3anidm  1121  3an4anass  1122  3ioran  1123  3ianor  1124  3impa  1127  3expa  1136  3jca  1146  3anbi123i  1173  3pm3.2i  1358  3jaob  1454  3anbi123d  1465  3anim123d  1472  an6  1475  an3andi  1514  an33rean  1515  cadan  1642  19.26-3an  1905  hb3an  1907  nf3and  1933  nf3an  1936  4exdistr  1996  sb3an  2120  eeeanv  2383  mopick2  2665  r19.26-3  3127  r3al  3204  r3ex  3205  rexlimdvvva  3224  3reeanv  3239  ceqsex3v  3506  ceqsex4v  3507  ceqsex8v  3509  rspc4v  3599  sbc3an  3806  elin3  4106  rexdifpr  4620  raltpg  4659  tpss  4795  opthprneg  4823  dfopif  4840  disjxun  5104  otth2  5456  otthg  5458  oteqex  5476  poirr  5575  po3nr  5578  wefrc  5649  otelxp  5699  rabxp  5703  f1orn  6854  2f1fvneq  7284  fpropnf1  7291  dff1o6  7303  oprabidw  7471  oprabid  7472  oprabv  7500  ndmovass  7630  elovmpo  7687  elovmporab  7688  elovmporab1w  7689  elovmporab1  7690  elovmpt3rab1  7702  dfwe2  7809  opiota  8092  dfxp3  8094  bropopvvv  8123  poxp2  8184  xpord2pred  8186  xpord3pred  8193  sexp3  8194  oaord  8580  oeeu  8637  nnaord  8653  naddasslem1  8729  swoso  8777  fiint  9343  funsnfsupp  9408  ttrclselem2  9751  alephval3  10213  ingru  10924  axgroth3  10940  ltrelxr  11394  ltxrlt  11404  wloglei  11872  sup2  12297  rexuz2  13050  ltxr  13268  elixx3g  13513  ixxun  13516  dfrp2  13549  elioo4g  13561  elioopnf  13598  elioomnf  13599  elicopnf  13600  elxrge0  13612  divelunit  13649  elfz2  13670  elfzuzb  13674  uzsplit  13754  fznn0  13777  elfzmlbp  13797  preduz  13808  elfzo2  13820  fzolb2  13825  fzouzsplit  13853  ssfzo12bi  13920  fzind2  13947  hashgt23el  14593  ccatsymb  14752  swrdsbslen  14839  swrdspsleq  14840  swrdccatin2  14903  pfxccatin12lem2  14905  pfxccatin12lem3  14906  pfxccatin12  14907  pfxccat3a  14912  repsdf2  14954  repswsymball  14955  repswsymballbi  14956  repswswrd  14960  s3eq3seq  15116  wrdl3s3  15141  s3sndisj  15146  s3iunsndisj  15147  abs2dif  15526  sinltx  16383  divalglem8  16596  divalglem10  16598  divalgb  16600  bitsval2  16621  divgcdz  16709  rplpwr  16758  cncongr1  16868  pythagtriplem2  17021  pythagtrip  17038  prmgaplem4  17258  isstruct  17356  setsstruct2  17378  imasvscafn  17735  xpscf  17763  mreexmrid  17843  iscatd2  17881  issect  17954  issect2  17955  oppcsect  17979  isfunc  18065  funcpropd  18103  fucsect  18176  fucinv  18177  initoeu2  18217  setcsect  18290  setcinv  18291  issgrpd  18945  ismhm0  19011  issubm2  19025  issubg3  19381  resgrpisgrp  19384  eqgval  19415  eqger  19416  qusxpid  19421  cycsubgcl  19447  isgim  19502  gim0to0  19509  gaorb  19548  gaorber  19549  gastacos  19551  symg2bas  19634  galactghm  19645  pmtr3ncom  19716  ispgp  19833  efgcpbllema  19995  efgcpbllemb  19996  eqgabl  20075  qusecsub  20076  cygabl  20132  dprdw  20253  omndmul2  20374  rnglz  20414  rngpropd  20423  ringpropd  20546  ringrghm  20571  isirred2  20678  rngcsect  20915  rngcinv  20916  ringcsect  20949  ringcinv  20950  isdrng5  21035  drngid2  21037  issdrg2  21079  isorng  21145  islss  21236  islmim  21364  lmhmpropd  21375  prmidl0  21661  zndvds  21882  znleval  21887  znleval2  21888  obselocv  22061  lindsenlbs  22184  mpfrcl  22421  matinvgcell  22777  mat1dimscm  22817  scmatscm  22855  scmatf1  22873  mdetunilem7  22960  matunitlindflem2  23022  cpmatacl  23061  cpmatmcl  23064  mat2pmatf1  23074  mat2pmatghm  23075  mat2pmatmul  23076  mat2pmatlin  23080  mat2pmatscmxcl  23085  m2pmfzgsumcl  23093  decpmataa0  23113  monmatcollpw  23124  pmatcollpwscmatlem1  23134  pmatcollpwscmatlem2  23135  pm2mpghm  23161  pm2mpmhmlem2  23164  monmat2matmon  23169  chfacfisf  23199  chfacfisfcpmat  23200  chfacfpmmulgsum2  23210  isbasis3g  23294  leordtvallem2  23556  lmfval  23577  lmbr  23603  lmbr2  23604  lmmo  23725  dfconn2  23764  ptbasin  23923  ptbasfi  23927  txcnpi  23954  ptcnp  23968  hausdiag  23991  qtophmeo  24163  fbunfip  24215  elflim2  24310  hausflimi  24326  isfcls  24355  isfcls2  24359  istmd  24420  istgp  24423  istrg  24510  istdrg  24512  istdrg2  24524  istlm  24531  imasdsf1olem  24719  xmeterval  24778  xmeter  24779  prdsxmslem2  24875  blval2  24908  isngp  24942  isngp2  24943  isngp3  24944  isnlm  25021  cnbl0  25119  cnblcld  25120  elii1  25283  isphtpc  25342  phtpcer  25343  isclmp  25445  iscph  25518  lmmbr  25606  lmmbr2  25607  lmmbrf  25610  iscfil2  25614  iscau3  25626  iscau4  25627  iscauf  25628  caucfil  25631  isbn  25686  ishl2  25718  ovolfcl  25814  ioombl1lem4  25909  mbfmax  25997  iblpos  26140  limcrcl  26221  ig1pval3  26523  ulmdvlem3  26756  ellogdm  26994  relogbcl  27128  fsumvma2  27568  chpchtsum  27573  chpub  27574  dchrelbas3  27592  gausslemma2dlem1a  27719  noetalem1  28125  sltssnb  28182  eqcuts  28198  eqcuts2  28199  lnhl  29108  colopp  29274  dfcgra2  29365  axeuclidlem  29567  axeuclid  29568  edgupgr  29739  umgr2edg1  29819  subusgr  29897  nbgrel  29948  nb3grpr2  29991  nb3gr2nb  29992  isuvtx  30003  nbupgruvtxres  30015  iscplgredg  30025  cplgr3v  30043  rusgrpropedg  30192  rgrusgrprc  30197  rusgrprc  30198  upgriswlk  30248  wlkonprop  30264  subgrwlk  30296  wksonproplem  30314  usgr2pth0  30378  isclwlke  30391  crctcshtrl  30439  iswwlksnx  30456  wwlknbp  30458  2trld  30554  rusgrnumwwlkl1  30587  rusgrnumwwlkb0  30590  rusgrnumwwlk  30594  clwlkclwwlkflem  30622  erclwwlkref  30638  clwwlkwwlksb  30672  erclwwlknref  30687  clwwlknon2x  30721  0wlk  30734  loop1cycl  30771  3spthd  30804  umgr3v3e3cycl  30812  frgr3v  30903  1to3vfriswmgr  30908  frgr2wwlkeu  30955  numclwwlk1lem2fo  30986  dlwwlknondlwlknonf1o  30993  nvex  31240  isnv  31241  dfadj2  32514  cnvadj  32521  adjeq  32564  eleigvec  32586  eleigvec2  32587  chirredi  33023  or3di  33126  tpssg  33202  eliccelico  33436  pmtrprfv2  33716  fzto1st  33731  psgnfzto1st  33733  qusker  33977  lsmsnorb  34013  mxidlirred  34064  ply1degltel  34193  ply1degleel  34194  eulerpartlemv  35063  eulerpartlemd  35065  eulerpartlemn  35080  prob01  35112  probun  35118  bnj170  35396  bnj248  35398  bnj252  35401  bnj253  35402  bnj945  35471  bnj1098  35481  bnj1224  35498  bnj150  35573  bnj153  35577  bnj545  35592  bnj557  35598  bnj571  35603  bnj594  35609  bnj864  35619  bnj865  35620  bnj849  35622  bnj964  35640  bnj986  35652  bnj996  35653  bnj1033  35666  bnj1110  35679  bnj1128  35687  bnj1174  35700  acwer1prclem  35850  onprcf1acwevdlem1  36044  cusgr3cyclex  36067  2cycl2d  36068  pconnconn  36162  resconn  36177  iscvm  36190  cvmlift2lem12  36245  cvmlift3lem5  36254  satfdm  36300  elmpst  36467  mpstrcl  36472  lediv2aALT  36608  3jcadALT  36618  mirimanofffr  36628  dfso3  36662  br6  36699  elfuns  36854  brimg  36876  lemsuccf  36880  cgrxfr  36997  segcon2  37047  seglecgr12im  37052  seglecgr12  37053  segletr  37056  btwnoutside  37067  broutsideof3  37068  outsideoftr  37071  outsidele  37074  bj-imn3ani  37634  relowlpssretop  38478  wl-df3-3mintru2  38600  fdc  38870  isbnd3b  38910  ablo4pnp  39005  crngm4  39128  isidlc  39140  pridl  39162  ispridl2  39163  ispridlc  39195  ts3an1  39273  ts3an2  39274  ts3an3  39275  brres2  39396  disjressuc2  39534  xrninxp  39538  dfsuccl4  39597  dfeqvrels2  39795  dfeqvrel2  39797  dfeqvrel3  39798  dfeldisj3  39934  islshpsm  40228  islshpat  40265  cmtfvalN  40458  cmtvalN  40459  ishlat1  40600  ishlat2  40601  3dim0  40705  2dim  40718  islvol5  40827  lhpexle3  41260  cdleme0ex2N  41472  cdleme0nex  41538  cdlemg2cex  41839  cdlemg33b0  41949  cdlemg33b  41955  cdlemg33c  41956  cdlemg33e  41958  dib1dim  42413  diblsmopel  42419  dihopelvalcpre  42496  lcfls1c  42784  aks6d1c1p1  43348  aks6d1c1p1rcl  43349  sn-sup2  43746  sn-isghm  43875  3anrabdioph  43984  fgraphxp  44396  omge2  44490  faosnf0.11b  44618  dfsucon  44714  pren2  44744  dfrtrcl5  44819  brfvrcld2  44882  df3an2  44959  dfvd3  45763  3impexpVD  46027  modelaxreplem1  46161  rfcnnnub  46256  stoweidlem35  47248  smflimlem4  47987  ndmaovass  48479  nltle2tri  48586  elfz2z  48588  prproropf1olem0  48787  reuprpr  48808  gboge9  49065  sbgoldbalt  49082  nnsum4primesodd  49097  nnsum4primesoddALTV  49098  bgoldbtbndlem4  49109  bgoldbtbnd  49110  dfvopnbgr2  49154  isuspgrim  49197  isubgr3stgrlem7  49273  grlimprop2  49287  uhgrimgrlim  49288  pgn4cyclex  49427  rngcsectALTV  49575  rngcinvALTV  49576  ringcsectALTV  49609  ringcinvALTV  49610  islindeps  49768  islindeps2  49798  isldepslvec2  49800  elbigo2  49867  line2ylem  50066  io1ii  50238  catprsc  50330  0funcglem  50401  0funclem  50404  catcsect  50736  isthincd2  50775  thincsect  50805  2arwcatlem1  50936