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  1453  3anbi123d  1464  3anim123d  1471  an6  1474  an3andi  1513  an33rean  1514  cadan  1641  19.26-3an  1904  nf3and  1930  nf3an  1933  4exdistr  1993  sb3an  2117  eeeanv  2379  mopick2  2662  r19.26-3  3123  r3al  3200  r3ex  3201  rexlimdvvva  3220  3reeanv  3235  ceqsex3v  3502  ceqsex4v  3503  ceqsex8v  3505  rspc4v  3595  sbc3an  3802  elin3  4103  rexdifpr  4619  raltpg  4658  tpss  4796  opthprneg  4824  dfopif  4829  disjxun  5100  otth2  5451  otthg  5453  oteqex  5471  poirr  5570  po3nr  5573  wefrc  5644  otelxp  5694  rabxp  5698  f1orn  6835  2f1fvneq  7264  fpropnf1  7271  dff1o6  7283  oprabidw  7451  oprabid  7452  oprabv  7480  ndmovass  7609  elovmpo  7666  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  elovmpt3rab1  7681  dfwe2  7788  opiota  8070  dfxp3  8072  bropopvvv  8101  poxp2  8160  xpord2pred  8162  xpord3pred  8169  sexp3  8170  oaord  8555  oeeu  8612  nnaord  8628  naddasslem1  8704  swoso  8752  fiint  9318  funsnfsupp  9384  ttrclselem2  9727  alephval3  10189  ingru  10900  axgroth3  10916  ltrelxr  11370  ltxrlt  11380  wloglei  11848  sup2  12273  rexuz2  13026  ltxr  13244  elixx3g  13489  ixxun  13492  dfrp2  13525  elioo4g  13537  elioopnf  13574  elioomnf  13575  elicopnf  13576  elxrge0  13588  divelunit  13625  elfz2  13646  elfzuzb  13650  uzsplit  13730  fznn0  13753  elfzmlbp  13773  preduz  13784  elfzo2  13796  fzolb2  13801  fzouzsplit  13829  ssfzo12bi  13896  fzind2  13923  hashgt23el  14569  ccatsymb  14728  swrdsbslen  14814  swrdspsleq  14815  swrdccatin2  14878  pfxccatin12lem2  14880  pfxccatin12lem3  14881  pfxccatin12  14882  pfxccat3a  14887  repsdf2  14929  repswsymball  14930  repswsymballbi  14931  repswswrd  14935  s3eq3seq  15090  wrdl3s3  15115  s3sndisj  15120  s3iunsndisj  15121  abs2dif  15500  sinltx  16357  divalglem8  16570  divalglem10  16572  divalgb  16574  bitsval2  16595  divgcdz  16683  rplpwr  16732  cncongr1  16842  pythagtriplem2  16995  pythagtrip  17012  prmgaplem4  17232  isstruct  17330  setsstruct2  17352  imasvscafn  17709  xpscf  17737  mreexmrid  17817  iscatd2  17855  issect  17928  issect2  17929  oppcsect  17953  isfunc  18039  funcpropd  18077  fucsect  18150  fucinv  18151  initoeu2  18191  setcsect  18264  setcinv  18265  issgrpd  18919  ismhm0  18985  issubm2  18999  issubg3  19355  resgrpisgrp  19358  eqgval  19389  eqger  19390  qusxpid  19395  cycsubgcl  19421  isgim  19476  gim0to0  19483  gaorb  19521  gaorber  19522  gastacos  19524  symg2bas  19607  galactghm  19618  pmtr3ncom  19689  ispgp  19806  efgcpbllema  19968  efgcpbllemb  19969  eqgabl  20048  qusecsub  20049  cygabl  20105  dprdw  20226  omndmul2  20347  rnglz  20387  rngpropd  20396  ringpropd  20519  ringrghm  20544  isirred2  20651  rngcsect  20888  rngcinv  20889  ringcsect  20922  ringcinv  20923  isdrng5  21008  drngid2  21010  issdrg2  21052  isorng  21118  islss  21209  islmim  21337  lmhmpropd  21348  prmidl0  21634  zndvds  21855  znleval  21860  znleval2  21861  obselocv  22034  lindsenlbs  22157  mpfrcl  22394  matinvgcell  22750  mat1dimscm  22790  scmatscm  22828  scmatf1  22846  mdetunilem7  22933  matunitlindflem2  22995  cpmatacl  23034  cpmatmcl  23037  mat2pmatf1  23047  mat2pmatghm  23048  mat2pmatmul  23049  mat2pmatlin  23053  mat2pmatscmxcl  23058  m2pmfzgsumcl  23066  decpmataa0  23086  monmatcollpw  23097  pmatcollpwscmatlem1  23107  pmatcollpwscmatlem2  23108  pm2mpghm  23134  pm2mpmhmlem2  23137  monmat2matmon  23142  chfacfisf  23172  chfacfisfcpmat  23173  chfacfpmmulgsum2  23183  isbasis3g  23267  leordtvallem2  23529  lmfval  23550  lmbr  23576  lmbr2  23577  lmmo  23698  dfconn2  23737  ptbasin  23896  ptbasfi  23900  txcnpi  23927  ptcnp  23941  hausdiag  23964  qtophmeo  24136  fbunfip  24188  elflim2  24283  hausflimi  24299  isfcls  24328  isfcls2  24332  istmd  24393  istgp  24396  istrg  24483  istdrg  24485  istdrg2  24497  istlm  24504  imasdsf1olem  24692  xmeterval  24751  xmeter  24752  prdsxmslem2  24848  blval2  24881  isngp  24915  isngp2  24916  isngp3  24917  isnlm  24994  cnbl0  25092  cnblcld  25093  elii1  25256  isphtpc  25315  phtpcer  25316  isclmp  25418  iscph  25491  lmmbr  25579  lmmbr2  25580  lmmbrf  25583  iscfil2  25587  iscau3  25599  iscau4  25600  iscauf  25601  caucfil  25604  isbn  25659  ishl2  25691  ovolfcl  25787  ioombl1lem4  25882  mbfmax  25970  iblpos  26113  limcrcl  26194  ig1pval3  26496  ulmdvlem3  26729  ellogdm  26967  relogbcl  27101  fsumvma2  27541  chpchtsum  27546  chpub  27547  dchrelbas3  27565  gausslemma2dlem1a  27692  noetalem1  28098  sltssnb  28155  eqcuts  28171  eqcuts2  28172  lnhl  29081  colopp  29247  dfcgra2  29338  axeuclidlem  29540  axeuclid  29541  edgupgr  29712  umgr2edg1  29792  subusgr  29870  nbgrel  29921  nb3grpr2  29964  nb3gr2nb  29965  isuvtx  29976  nbupgruvtxres  29988  iscplgredg  29998  cplgr3v  30016  rusgrpropedg  30165  rgrusgrprc  30170  rusgrprc  30171  upgriswlk  30221  wlkonprop  30237  subgrwlk  30269  wksonproplem  30287  usgr2pth0  30351  isclwlke  30364  crctcshtrl  30412  iswwlksnx  30429  wwlknbp  30431  2trld  30527  rusgrnumwwlkl1  30560  rusgrnumwwlkb0  30563  rusgrnumwwlk  30567  clwlkclwwlkflem  30595  erclwwlkref  30611  clwwlkwwlksb  30645  erclwwlknref  30660  clwwlknon2x  30694  0wlk  30707  loop1cycl  30744  3spthd  30777  umgr3v3e3cycl  30785  frgr3v  30876  1to3vfriswmgr  30881  frgr2wwlkeu  30928  numclwwlk1lem2fo  30959  dlwwlknondlwlknonf1o  30966  nvex  31213  isnv  31214  dfadj2  32487  cnvadj  32494  adjeq  32537  eleigvec  32559  eleigvec2  32560  chirredi  32996  or3di  33099  tpssg  33175  eliccelico  33411  pmtrprfv2  33691  fzto1st  33706  psgnfzto1st  33708  qusker  33952  lsmsnorb  33988  mxidlirred  34039  ply1degltel  34168  ply1degleel  34169  eulerpartlemv  35038  eulerpartlemd  35040  eulerpartlemn  35055  prob01  35087  probun  35093  bnj170  35371  bnj248  35373  bnj252  35376  bnj253  35377  bnj945  35446  bnj1098  35456  bnj1224  35473  bnj150  35548  bnj153  35552  bnj545  35567  bnj557  35573  bnj571  35578  bnj594  35584  bnj864  35594  bnj865  35595  bnj849  35597  bnj964  35615  bnj986  35627  bnj996  35628  bnj1033  35641  bnj1110  35654  bnj1128  35662  bnj1174  35675  acwer1prclem  35801  onprcf1acwevdlem1  35937  cusgr3cyclex  35953  2cycl2d  35954  pconnconn  36038  resconn  36053  iscvm  36066  cvmlift2lem12  36121  cvmlift3lem5  36130  satfdm  36176  elmpst  36343  mpstrcl  36348  lediv2aALT  36484  3jcadALT  36494  dfso3  36527  br6  36564  elfuns  36719  brimg  36741  lemsuccf  36745  cgrxfr  36862  segcon2  36912  seglecgr12im  36917  seglecgr12  36918  segletr  36921  btwnoutside  36932  broutsideof3  36933  outsideoftr  36936  outsidele  36939  bj-imn3ani  37499  relowlpssretop  38330  wl-df3-3mintru2  38452  fdc  38722  isbnd3b  38762  ablo4pnp  38857  crngm4  38980  isidlc  38992  pridl  39014  ispridl2  39015  ispridlc  39047  ts3an1  39125  ts3an2  39126  ts3an3  39127  brres2  39248  disjressuc2  39386  xrninxp  39390  dfsuccl4  39449  dfeqvrels2  39647  dfeqvrel2  39649  dfeqvrel3  39650  dfeldisj3  39786  islshpsm  40080  islshpat  40117  cmtfvalN  40310  cmtvalN  40311  ishlat1  40452  ishlat2  40453  3dim0  40557  2dim  40570  islvol5  40679  lhpexle3  41112  cdleme0ex2N  41324  cdleme0nex  41390  cdlemg2cex  41691  cdlemg33b0  41801  cdlemg33b  41807  cdlemg33c  41808  cdlemg33e  41810  dib1dim  42265  diblsmopel  42271  dihopelvalcpre  42348  lcfls1c  42636  aks6d1c1p1  43200  aks6d1c1p1rcl  43201  sn-sup2  43598  sn-isghm  43727  3anrabdioph  43835  fgraphxp  44248  omge2  44342  faosnf0.11b  44470  dfsucon  44566  pren2  44596  dfrtrcl5  44671  brfvrcld2  44734  df3an2  44811  dfvd3  45616  3impexpVD  45880  modelaxreplem1  46010  rfcnnnub  46095  stoweidlem35  47087  smflimlem4  47826  ndmaovass  48318  nltle2tri  48425  elfz2z  48427  prproropf1olem0  48626  reuprpr  48647  gboge9  48904  sbgoldbalt  48921  nnsum4primesodd  48936  nnsum4primesoddALTV  48937  bgoldbtbndlem4  48948  bgoldbtbnd  48949  dfvopnbgr2  48993  isuspgrim  49036  isubgr3stgrlem7  49112  grlimprop2  49126  uhgrimgrlim  49127  pgn4cyclex  49266  rngcsectALTV  49414  rngcinvALTV  49415  ringcsectALTV  49448  ringcinvALTV  49449  islindeps  49607  islindeps2  49637  isldepslvec2  49639  elbigo2  49706  line2ylem  49905  io1ii  50071  catprsc  50163  0funcglem  50233  0funclem  50236  catcsect  50548  isthincd2  50587  thincsect  50617  2arwcatlem1  50745