Definition df-3an 1104

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

This definition is used by:  3anass  1110  3anan32OLD  1113  3ancomb  1115  3anidm  1120  3an4anass  1121  3ioran  1122  3ianor  1123  3impa  1126  3expa  1135  3jca  1145  3anbi123i  1172  3pm3.2i  1357  3jaob  1452  3anbi123d  1463  3anim123d  1470  an6  1473  an3andi  1512  an33rean  1513  cadan  1638  19.26-3an  1901  nf3and  1927  nf3an  1930  4exdistr  1990  sb3an  2114  eeeanv  2381  mopick2  2664  r19.26-3  3125  r3al  3202  r3ex  3203  rexlimdvvva  3222  3reeanv  3237  ceqsex3v  3506  ceqsex4v  3507  ceqsex8v  3509  rspc4v  3600  sbc3an  3807  elin3  4158  rexdifpr  4624  raltpg  4663  tpss  4801  opthprneg  4829  dfopif  4834  disjxun  5106  otth2  5464  otthg  5466  oteqex  5482  poirr  5580  po3nr  5583  wefrc  5654  otelxp  5704  rabxp  5708  f1orn  6831  2f1fvneq  7258  fpropnf1  7265  dff1o6  7273  oprabidw  7443  oprabid  7444  oprabv  7472  ndmovass  7600  elovmpo  7657  elovmporab  7658  elovmporab1w  7659  elovmporab1  7660  elovmpt3rab1  7672  dfwe2  7771  opiota  8054  dfxp3  8056  bropopvvv  8083  poxp2  8137  xpord2pred  8139  xpord3pred  8146  sexp3  8147  oaord  8530  oeeu  8587  nnaord  8603  naddasslem1  8679  swoso  8727  fiint  9284  funsnfsupp  9350  ttrclselem2  9693  alephval3  10101  ingru  10806  axgroth3  10822  ltrelxr  11276  ltxrlt  11286  wloglei  11752  sup2  12177  rexuz2  12929  ltxr  13146  elixx3g  13391  ixxun  13394  dfrp2  13427  elioo4g  13439  elioopnf  13476  elioomnf  13477  elicopnf  13478  elxrge0  13490  divelunit  13527  elfz2  13548  elfzuzb  13552  uzsplit  13631  fznn0  13654  elfzmlbp  13674  preduz  13685  elfzo2  13697  fzolb2  13702  fzouzsplit  13730  ssfzo12bi  13797  fzind2  13824  hashgt23el  14468  ccatsymb  14627  swrdsbslen  14709  swrdspsleq  14710  swrdccatin2  14773  pfxccatin12lem2  14775  pfxccatin12lem3  14776  pfxccatin12  14777  pfxccat3a  14782  repsdf2  14822  repswsymball  14823  repswsymballbi  14824  repswswrd  14828  s3eq3seq  14983  wrdl3s3  15006  s3sndisj  15011  s3iunsndisj  15012  abs2dif  15391  sinltx  16251  divalglem8  16464  divalglem10  16466  divalgb  16468  bitsval2  16489  divgcdz  16575  rplpwr  16622  cncongr1  16731  pythagtriplem2  16883  pythagtrip  16900  prmgaplem4  17120  isstruct  17218  setsstruct2  17240  imasvscafn  17597  xpscf  17625  mreexmrid  17705  iscatd2  17743  issect  17816  issect2  17817  oppcsect  17841  isfunc  17927  funcpropd  17965  fucsect  18038  fucinv  18039  initoeu2  18079  setcsect  18152  setcinv  18153  issgrpd  18794  ismhm0  18854  issubm2  18868  issubg3  19217  resgrpisgrp  19220  eqgval  19251  eqger  19252  qusxpid  19257  cycsubgcl  19283  isgim  19338  gim0to0  19345  gaorb  19383  gaorber  19384  gastacos  19386  symg2bas  19469  galactghm  19480  pmtr3ncom  19551  ispgp  19668  efgcpbllema  19830  efgcpbllemb  19831  eqgabl  19910  qusecsub  19911  cygabl  19967  dprdw  20088  omndmul2  20209  rnglz  20249  rngpropd  20258  ringpropd  20378  ringrghm  20403  isirred2  20510  rngcsect  20746  rngcinv  20747  ringcsect  20780  ringcinv  20781  isdrng5  20865  drngid2  20867  issdrg2  20909  isorng  20975  islss  21066  islmim  21194  lmhmpropd  21205  prmidl0  21489  zndvds  21710  znleval  21715  znleval2  21716  obselocv  21889  mpfrcl  22247  matinvgcell  22603  mat1dimscm  22643  scmatscm  22681  scmatf1  22699  mdetunilem7  22786  cpmatacl  22884  cpmatmcl  22887  mat2pmatf1  22897  mat2pmatghm  22898  mat2pmatmul  22899  mat2pmatlin  22903  mat2pmatscmxcl  22908  m2pmfzgsumcl  22916  decpmataa0  22936  monmatcollpw  22947  pmatcollpwscmatlem1  22957  pmatcollpwscmatlem2  22958  pm2mpghm  22984  pm2mpmhmlem2  22987  monmat2matmon  22992  chfacfisf  23022  chfacfisfcpmat  23023  chfacfpmmulgsum2  23033  isbasis3g  23117  leordtvallem2  23379  lmfval  23400  lmbr  23426  lmbr2  23427  lmmo  23548  dfconn2  23587  ptbasin  23745  ptbasfi  23749  txcnpi  23776  ptcnp  23790  hausdiag  23813  qtophmeo  23985  fbunfip  24037  elflim2  24132  hausflimi  24148  isfcls  24177  isfcls2  24181  istmd  24242  istgp  24245  istrg  24332  istdrg  24334  istdrg2  24346  istlm  24353  imasdsf1olem  24541  xmeterval  24600  xmeter  24601  prdsxmslem2  24697  blval2  24730  isngp  24764  isngp2  24765  isngp3  24766  isnlm  24843  cnbl0  24941  cnblcld  24942  elii1  25105  isphtpc  25164  phtpcer  25165  isclmp  25267  iscph  25340  lmmbr  25428  lmmbr2  25429  lmmbrf  25432  iscfil2  25436  iscau3  25448  iscau4  25449  iscauf  25450  caucfil  25453  isbn  25508  ishl2  25540  ovolfcl  25636  ioombl1lem4  25731  mbfmax  25819  iblpos  25963  limcrcl  26044  ig1pval3  26346  ulmdvlem3  26576  ellogdm  26815  relogbcl  26949  fsumvma2  27389  chpchtsum  27394  chpub  27395  dchrelbas3  27413  gausslemma2dlem1a  27540  noetalem1  27916  sltssnb  27973  eqcuts  27989  eqcuts2  27990  lnhl  28898  colopp  29062  dfcgra2  29152  axeuclidlem  29323  axeuclid  29324  edgupgr  29495  umgr2edg1  29572  subusgr  29650  nbgrel  29701  nb3grpr2  29744  nb3gr2nb  29745  isuvtx  29756  nbupgruvtxres  29768  iscplgredg  29778  cplgr3v  29796  rusgrpropedg  29945  rgrusgrprc  29950  rusgrprc  29951  upgriswlk  30001  wlkonprop  30017  wksonproplem  30063  usgr2pth0  30125  isclwlke  30137  crctcshtrl  30183  iswwlksnx  30200  wwlknbp  30202  2trld  30298  rusgrnumwwlkl1  30331  rusgrnumwwlkb0  30334  rusgrnumwwlk  30338  clwlkclwwlkflem  30366  erclwwlkref  30382  clwwlkwwlksb  30416  erclwwlknref  30431  clwwlknon2x  30465  0wlk  30478  3spthd  30538  umgr3v3e3cycl  30546  frgr3v  30637  1to3vfriswmgr  30642  frgr2wwlkeu  30689  numclwwlk1lem2fo  30720  dlwwlknondlwlknonf1o  30727  nvex  30974  isnv  30975  dfadj2  32248  cnvadj  32255  adjeq  32298  eleigvec  32320  eleigvec2  32321  chirredi  32757  or3di  32818  tpssg  32894  eliccelico  33133  pmtrprfv2  33417  fzto1st  33432  psgnfzto1st  33434  qusker  33678  lsmsnorb  33713  mxidlirred  33764  ply1degltel  33893  ply1degleel  33894  eulerpartlemv  34763  eulerpartlemd  34765  eulerpartlemn  34780  prob01  34812  probun  34818  bnj170  35096  bnj248  35098  bnj252  35101  bnj253  35102  bnj945  35171  bnj1098  35181  bnj1224  35198  bnj150  35273  bnj153  35277  bnj545  35292  bnj557  35298  bnj571  35303  bnj594  35309  bnj864  35319  bnj865  35320  bnj849  35322  bnj964  35340  bnj986  35352  bnj996  35353  bnj1033  35366  bnj1110  35379  bnj1128  35387  bnj1174  35400  subgrwlk  35632  cusgr3cyclex  35636  loop1cycl  35637  2cycl2d  35639  pconnconn  35731  resconn  35746  iscvm  35759  cvmlift2lem12  35814  cvmlift3lem5  35823  satfdm  35869  elmpst  36036  mpstrcl  36041  lediv2aALT  36177  3jcadALT  36187  dfso3  36220  br6  36257  elfuns  36413  brimg  36435  lemsuccf  36439  cgrxfr  36555  segcon2  36605  seglecgr12im  36610  seglecgr12  36611  segletr  36614  btwnoutside  36625  broutsideof3  36626  outsideoftr  36629  outsidele  36632  bj-imn3ani  37208  relowlpssretop  38038  wl-df3-3mintru2  38160  lindsenlbs  38294  matunitlindflem2  38296  fdc  38424  isbnd3b  38464  ablo4pnp  38559  crngm4  38682  isidlc  38694  pridl  38716  ispridl2  38717  ispridlc  38749  ts3an1  38827  ts3an2  38828  ts3an3  38829  brres2  38950  disjressuc2  39088  xrninxp  39092  dfsuccl4  39151  dfeqvrels2  39349  dfeqvrel2  39351  dfeqvrel3  39352  dfeldisj3  39488  islshpsm  39782  islshpat  39819  cmtfvalN  40012  cmtvalN  40013  ishlat1  40154  ishlat2  40155  3dim0  40259  2dim  40272  islvol5  40381  lhpexle3  40814  cdleme0ex2N  41026  cdleme0nex  41092  cdlemg2cex  41393  cdlemg33b0  41503  cdlemg33b  41509  cdlemg33c  41510  cdlemg33e  41512  dib1dim  41967  diblsmopel  41973  dihopelvalcpre  42050  lcfls1c  42338  aks6d1c1p1  42902  aks6d1c1p1rcl  42903  sn-sup2  43293  sn-isghm  43433  3anrabdioph  43541  fgraphxp  43959  omge2  44053  faosnf0.11b  44181  dfsucon  44277  pren2  44307  dfrtrcl5  44383  brfvrcld2  44446  df3an2  44523  dfvd3  45328  3impexpVD  45592  modelaxreplem1  45715  rfcnnnub  45784  stoweidlem35  46777  smflimlem4  47516  ndmaovass  47971  nltle2tri  48078  elfz2z  48080  prproropf1olem0  48279  reuprpr  48300  gboge9  48557  sbgoldbalt  48574  nnsum4primesodd  48589  nnsum4primesoddALTV  48590  bgoldbtbndlem4  48601  bgoldbtbnd  48602  dfvopnbgr2  48646  isuspgrim  48689  isubgr3stgrlem7  48765  grlimprop2  48779  uhgrimgrlim  48780  pgn4cyclex  48919  rngcsectALTV  49068  rngcinvALTV  49069  ringcsectALTV  49102  ringcinvALTV  49103  islindeps  49261  islindeps2  49291  isldepslvec2  49293  elbigo2  49360  line2ylem  49559  io1ii  49727  catprsc  49819  0funcglem  49889  0funclem  49892  catcsect  50204  isthincd2  50243  thincsect  50273  2arwcatlem1  50401