MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-3an Unicode version

Definition df-3an 975
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 649. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
df-3an

Detailed syntax breakdown of Definition df-3an
StepHypRef Expression
1 wph . . 3
2 wps . . 3
3 wch . . 3
41, 2, 3w3a 973 . 2
51, 2wa 369 . . 3
65, 3wa 369 . 2
74, 6wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  3anass  977  3anrot  978  3ancoma  980  3anan32  985  3anor  989  3ioran  991  3simpa  993  3pm3.2i  1174  pm3.2an3  1175  3jca  1176  3anbi123i  1185  3imp  1190  3an4anass  1219  3anbi123d  1299  3anim123d  1306  an6  1308  an3andi  1341  an33rean  1342  cadan  1459  19.26-3an  1682  4exdistr  1781  nf3and  1926  nf3an  1930  eeeanv  1989  sb3an  2141  mopick2  2362  r3al  2837  r19.26-3  2986  3reeanv  3026  ceqsex3v  3149  ceqsex4v  3150  ceqsex8v  3152  sbc3an  3390  elin3  3689  raltpg  4080  tpss  4195  dfopif  4214  disjxun  4450  otth2  4733  otthg  4735  oteqex  4745  poirr  4816  po3nr  4819  wefrc  4878  rabxp  5041  brinxp2  5066  brinxp  5067  f1orn  5831  dff1o6  6181  oprabid  6323  oprabv  6345  ndmovass  6463  elovmpt2  6520  elovmpt2rab  6521  elovmpt2rab1  6522  elovmpt3rab1  6536  dfwe2  6617  opiota  6859  dfxp3  6860  bropopvvv  6880  oaord  7215  oeeu  7271  nnaord  7287  swoso  7361  fiint  7817  funsnfsupp  7873  alephval3  8512  fpwwe2lem8  9036  fpwwe2lem9  9037  fpwwe2lem12  9040  ingru  9214  axgroth3  9230  ltrelxr  9669  ltxrlt  9676  wloglei  10110  sup2  10524  rexuz2  11161  ltxr  11353  elixx3g  11571  ixxun  11574  elioo4g  11614  elioopnf  11647  elioomnf  11648  elicopnf  11649  elxrge0  11658  divelunit  11691  elfz2  11708  elfzuzb  11711  uzsplit  11779  fznn0  11799  elfzmlbp  11815  elfzo2  11832  fzolb2  11835  fzouzsplit  11860  ssfzo12bi  11907  fzind2  11924  ccatsymb  12600  swrdccatin2  12712  swrdccatin12lem2  12714  swrdccatin12lem3  12715  swrdccatin12  12716  repsdf2  12750  repswsymball  12751  repswsymballbi  12752  repswswrd  12756  abs2dif  13165  sinltx  13924  divalglem8  14058  divalglem10  14060  divalgb  14062  bitsval2  14075  rplpwr  14194  pythagtriplem2  14341  pythagtrip  14358  pwsle  14889  imasvscafn  14934  mreexmrid  15040  iscatd2  15078  issect  15148  issect2  15149  oppcsect  15168  isfunc  15233  funcpropd  15269  fucsect  15341  fucinv  15342  setcsect  15416  setcinv  15417  issubm2  15979  issubg3  16219  resgrpisgrp  16222  cycsubgcl  16227  eqgval  16250  eqger  16251  isgim  16310  gaorb  16345  gaorber  16346  gastacos  16348  symg2bas  16423  galactghm  16428  gsmsymgreqlem2  16456  pmtr3ncom  16500  ispgp  16612  efgcpbllema  16772  efgcpbllemb  16773  eqgabl  16843  dprdw  17043  dprdwOLD  17050  ringpropd  17230  ringrghm  17251  isirred2  17350  rim0to0  17391  drngid2  17412  islss  17581  islmim  17708  lmhmpropd  17719  isassa  17964  mpfrcl  18187  zndvds  18588  znleval  18593  znleval2  18594  obselocv  18759  matinvgcell  18937  mat1dimscm  18977  scmatscm  19015  scmatf1  19033  mdetunilem7  19120  cpmatacl  19217  cpmatmcl  19220  mat2pmatf1  19230  mat2pmatghm  19231  mat2pmatmul  19232  mat2pmatlin  19236  mat2pmatscmxcl  19241  m2pmfzgsumcl  19249  decpmataa0  19269  monmatcollpw  19280  pmatcollpwscmatlem1  19290  pmatcollpwscmatlem2  19291  pm2mpghm  19317  pm2mpmhmlem2  19320  monmat2matmon  19325  chfacfisf  19355  chfacfisfcpmat  19356  chfacfpmmulgsum2  19366  isbasis3g  19450  leordtvallem2  19712  lmfval  19733  lmbr  19759  lmbr2  19760  lmmo  19881  dfcon2  19920  ptbasin  20078  ptbasfi  20082  txcnpi  20109  ptcnp  20123  hausdiag  20146  qtophmeo  20318  fbunfip  20370  elflim2  20465  hausflimi  20481  isfcls  20510  isfcls2  20514  istmd  20573  istgp  20576  istrg  20666  istdrg  20668  istdrg2  20680  istlm  20687  imasdsf1olem  20876  xmeterval  20935  xmeter  20936  prdsxmslem2  21032  blval2  21078  isngp  21116  isngp2  21117  isngp3  21118  isnlm  21184  cnbl0  21281  cnblcld  21282  elii1  21435  isphtpc  21494  phtpcer  21495  iscph  21617  lmmbr  21697  lmmbr2  21698  lmmbrf  21701  iscfil2  21705  iscau3  21717  iscau4  21718  iscauf  21719  caucfil  21722  isbn  21777  ishl2  21810  ovolfcl  21878  ioombl1lem4  21971  mbfmax  22056  iblpos  22199  limcrcl  22278  ig1pval3  22575  ulmdvlem3  22797  ellogdm  23020  fsumvma2  23489  chpchtsum  23494  chpub  23495  dchrelbas3  23513  axeuclidlem  24265  axeuclid  24266  nb3grapr2  24454  nb3gra2nb  24455  0wlk  24547  0trl  24548  constr2wlk  24600  3v3e3cycl1  24644  wwlknred  24723  wwlknndef  24737  isclwlk  24756  clwwlkprop  24770  clwwlknndef  24773  clwwlknwwlkncl  24800  wwlkext2clwwlk  24803  wwlksubclwwlk  24804  clwwnisshclwwn  24809  erclwwlkref  24813  erclwwlknref  24825  clwlkfoclwwlk  24845  el2wlkonotot0  24872  el2wlkonotot  24873  el2wlkonotot1  24874  2wlkonotv  24877  usg2spthonot0  24889  cusgraisrusgra  24938  rusgranumwlkl1  24947  rusgranumwlkb0  24953  rusgra0edg  24955  rusgranumwlk  24957  frgra3v  25002  1to3vfriswmgra  25007  frgraregorufrg  25072  extwwlkfablem2  25078  numclwwlkffin  25082  numclwwlkovfel2  25083  numclwwlkovf2  25084  numclwwlkovf2ex  25086  numclwwlkovgelim  25089  numclwlk1lem2fo  25095  numclwwlk2lem1  25102  numclwwlk7  25114  nvex  25504  isnv  25505  dfadj2  26804  cnvadj  26811  adjeq  26854  eleigvec  26876  eleigvec2  26877  chirredi  27313  or3di  27367  eliccelico  27588  omndmul2  27702  isorng  27789  relogbcl  28018  eulerpartlemv  28303  eulerpartlemd  28305  eulerpartlemn  28320  prob01  28352  probun  28358  pconcon  28676  rescon  28691  iscvm  28704  cvmlift2lem12  28759  cvmlift3lem5  28768  elmpst  28896  mpstrcl  28901  lediv2aALT  29043  dfso3  29097  br6  29186  preduz  29280  nofulllem2  29463  nofulllem5  29466  elfuns  29565  brimg  29587  brsuccf  29591  cgrxfr  29705  segcon2  29755  seglecgr12im  29760  seglecgr12  29761  segletr  29764  btwnoutside  29775  broutsideof3  29776  outsideoftr  29779  outsidele  29782  fdc  30238  isbnd3b  30281  ablo4pnp  30342  crngm4  30400  isidlc  30412  pridl  30434  ispridl2  30435  ispridlc  30467  ts3an1  30557  ts3an2  30558  ts3an3  30559  3anrabdioph  30716  issdrg2  31147  fgraphxp  31171  rfcnnnub  31411  stoweidlem35  31817  ndmaovass  32291  rexdifpr  32300  elfz2z  32331  usgra2pth0  32355  ismhm0  32493  initoeu2  32622  rnglz  32690  rngcsect  32788  rngcinv  32789  rngcsectOLD  32800  rngcinvOLD  32801  ringcsect  32839  ringcinv  32840  ringcsectOLD  32863  ringcinvOLD  32864  islindeps  33054  islindeps2  33084  isldepslvec2  33086  dfvd3  33368  3impexpVD  33656  bnj170  33750  bnj248  33752  bnj252  33755  bnj253  33756  bnj945  33832  bnj1098  33842  bnj1224  33860  bnj150  33934  bnj153  33938  bnj545  33953  bnj557  33959  bnj571  33964  bnj594  33970  bnj864  33980  bnj865  33981  bnj849  33983  bnj964  34001  bnj986  34012  bnj996  34013  bnj1033  34025  bnj1110  34038  bnj1128  34046  bnj1174  34059  bj-imn3ani  34176  islshpsm  34705  islshpat  34742  cmtfvalN  34935  cmtvalN  34936  ishlat1  35077  ishlat2  35078  3dim0  35181  2dim  35194  islvol5  35303  lhpexle3  35736  cdleme0ex2N  35949  cdleme0nex  36015  cdlemg2cex  36317  cdlemg33b0  36427  cdlemg33b  36433  cdlemg33c  36434  cdlemg33e  36436  dib1dim  36892  diblsmopel  36898  dihopelvalcpre  36975  lcfls1c  37263
  Copyright terms: Public domain W3C validator