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

Definition df-3an 941
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 632. (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 939 . 2
51, 2wa 360 . . 3
65, 3wa 360 . 2
74, 6wb 178 1
Colors of variables: wff set class
This definition is referenced by:  3anass  943  3anrot  944  3ancoma  946  3anan32  951  3anor  955  3ioran  957  3simpa  959  3pm3.2i  1140  pm3.2an3  1141  3jca  1142  3anbi123i  1150  3imp  1155  3anbi123d  1262  3anim123d  1269  an6  1271  cadan  1410  cadanOLD  1411  19.26-3an  1615  nf3and  1840  nf3an  1845  hb3anOLD  1849  4exdistr  1930  eeeanv  1934  eeeanvOLD  1935  sb3an  2142  mopick2  2392  r19.26-3  2886  3reeanv  2923  ceqsex3v  3044  ceqsex4v  3045  ceqsex8v  3047  sbc3an  3274  elin3  3565  raltpg  3944  tpss  4049  dfopif  4066  disjxun  4300  otth2  4578  oteqex  4588  poirr  4655  po3nr  4658  wefrc  4717  rabxp  4879  brinxp2  4904  brinxp  4905  f1orn  5645  dff1o6  5958  oprabid  6091  ndmovass  6218  elovmpt2  6274  dfwe2  6358  opiota  6594  dfxp3  6595  bropopvvv  6610  oaord  6902  oeeui  6957  oeeu  6958  nnaord  6974  swoso  7048  fiint  7495  alephval3  8105  fpwwe2lem8  8626  fpwwe2lem9  8627  fpwwe2lem12  8630  ingru  8804  axgroth3  8820  ltrelxr  9260  ltxrlt  9267  wloglei  9688  sup2  10095  rexuz2  10713  ltxr  10902  elixx3g  11120  ixxun  11123  elioo4g  11162  elioopnf  11189  elioomnf  11190  elicopnf  11191  elxrge0  11199  elfz2  11243  elfzuzb  11246  elfzmlbp  11290  fznn0  11319  uzsplit  11325  elfzo2  11351  fzolb2  11354  fzouzsplit  11379  ssfzo12bi  11414  fzind2  11429  ccatsymb  12068  swrdccatin2  12164  swrdccatin12lem2  12166  swrdccatin12lem3  12167  swrdccatin12  12168  repsdf2  12202  repswsymball  12203  repswsymballbi  12204  repswswrd  12208  abs2dif  12606  sinltx  13259  divalglem8  13390  divalglem10  13392  divalgb  13394  bitsval2  13407  rplpwr  13526  pythagtriplem2  13670  pythagtrip  13687  pwsle  14205  imasvscafn  14253  mreexmrid  14359  iscatd2  14397  issect  14470  issect2  14471  oppcsect  14490  isfunc  14552  funcpropd  14588  fucsect  14660  fucinv  14661  setcsect  14735  setcinv  14736  mndcl  15198  issubm2  15252  issubg3  15463  cycsubgcl  15469  eqgval  15492  eqger  15493  isgim  15552  gaorb  15587  gaorber  15588  gastacos  15590  galactghm  15609  ispgp  15729  efgcpbllema  15889  efgcpbllemb  15890  eqgabl  15957  dprdw  16071  rngpropd  16198  rngrghm  16215  isirred2  16309  drngid2  16354  islss  16514  islmim  16637  lmhmpropd  16648  isassa  16878  zndvds  17333  znleval  17338  znleval2  17339  obselocv  17458  isbasis3g  17517  leordtvallem2  17778  lmfval  17799  lmbr  17825  lmbr2  17826  lmmo  17947  dfcon2  17986  ptbasin  18113  ptbasfi  18117  txcnpi  18144  ptcnp  18158  hausdiag  18181  qtophmeo  18353  fbunfip  18405  elflim2  18500  hausflimi  18516  isfcls  18545  isfcls2  18549  istmd  18608  istgp  18611  istrg  18697  istdrg  18699  istdrg2  18711  istlm  18718  imasdsf1olem  18907  xmeterval  18966  xmeter  18967  prdsxmslem2  19063  blval2  19109  isngp  19147  isngp2  19148  isngp3  19149  isnlm  19215  cnbl0  19312  cnblcld  19313  elii1  19464  isphtpc  19523  phtpcer  19524  iscph  19637  lmmbr  19715  lmmbr2  19716  lmmbrf  19719  iscfil2  19723  iscau3  19735  iscau4  19736  iscauf  19737  caucfil  19740  isbn  19795  ishl2  19828  ovolfcl  19867  ioombl1lem4  19959  mbfmax  20043  iblpos  20186  limcrcl  20265  mpfrcl  20443  ig1pval3  20601  ulmdvlem3  20822  ellogdm  21039  fsumvma2  21507  chpchtsum  21512  chpub  21513  dchrelbas3  21531  nb3grapr2  21972  nb3gra2nb  21973  0wlk  22054  0trl  22055  constr2wlk  22107  3v3e3cycl1  22140  nvex  22599  isnv  22600  dfadj2  23899  cnvadj  23906  adjeq  23949  eleigvec  23971  eleigvec2  23972  chirredi  24408  or3di  24462  eliccelico  24688  omndmul2  24798  isorng  24919  relogbcl  25132  eulerpartlemv  25412  eulerpartlemd  25414  eulerpartlemn  25429  prob01  25437  probun  25443  pconcon  25757  rescon  25772  iscvm  25785  cvmlift2lem12  25840  cvmlift3lem5  25849  lediv2aALT  25953  dfso3  26007  divelunit  26015  br6  26210  preduz  26305  nofulllem2  26488  nofulllem5  26491  elfuns  26590  brimg  26612  brsuccf  26616  axeuclidlem  26731  axeuclid  26732  cgrxfr  26819  segcon2  26869  seglecgr12im  26874  seglecgr12  26875  segletr  26878  btwnoutside  26889  broutsideof3  26890  outsideoftr  26893  outsidele  26896  fdc  27312  isbnd3b  27357  ablo4pnp  27418  crngm4  27476  isidlc  27488  pridl  27510  ispridl2  27511  ispridlc  27543  ts3an1  27595  ts3an2  27596  ts3an3  27597  3anrabdioph  27772  issdrg2  28412  fgraphxp  28436  rfcnnnub  28608  stoweidlem35  28684  ndmaovass  28968  3an4anass  28971  rexdifpr  28982  otthg  28988  oprabv  29016  elovmpt2rab  29017  elovmpt2rab1  29018  elfz2z  29055  usgra2pth0  29161  wwlknred  29214  wwlknndef  29228  el2wlkonotot0  29250  el2wlkonotot  29251  el2wlkonotot1  29252  2wlkonotv  29255  usg2spthonot0  29267  isclwlk  29280  clwwlkprop  29292  clwwlknndef  29295  clwwlknwwlkncl  29321  wwlkext2clwwlk  29324  wwlksubclwwlk  29325  clwwnisshclwwn  29332  erclwwlkref  29342  erclwwlknref  29358  clwlkfoclwwlk  29377  cusgraisrusgra  29410  rusgranumwlkl1  29418  rusgranumwlkb0  29430  rusgra0edg  29432  rusgranumwlk  29434  frgra3v  29453  1to3vfriswmgra  29458  frgraregorufrg  29524  extwwlkfablem2  29530  numclwwlkffin  29534  numclwwlkovfel2  29535  numclwwlkovf2  29536  numclwwlkovf2ex  29538  numclwwlkovgelim  29541  numclwlk1lem2fo  29547  numclwwlk2lem1  29554  numclwwlk7  29566  symg2bas  29599  ex3  29849  dfvd3  29874  3impexpVD  30161  bnj170  30255  bnj248  30257  bnj252  30260  bnj253  30261  bnj945  30337  bnj1098  30347  bnj1224  30366  bnj150  30440  bnj153  30444  bnj545  30459  bnj557  30465  bnj571  30470  bnj594  30476  bnj864  30486  bnj865  30487  bnj849  30489  bnj964  30507  bnj986  30518  bnj996  30519  bnj1033  30531  bnj1110  30544  bnj1128  30552  bnj1174  30565  sb3anNEW11  30914  eeeanvOLD11  30978  islshpsm  31051  islshpat  31088  cmtfvalN  31281  cmtvalN  31282  ishlat1  31423  ishlat2  31424  3dim0  31527  2dim  31540  islvol5  31649  lhpexle3  32082  cdleme0ex2N  32294  cdleme0nex  32360  cdlemg2cex  32661  cdlemg33b0  32771  cdlemg33b  32777  cdlemg33c  32778  cdlemg33e  32780  dib1dim  33236  diblsmopel  33242  dihopelvalcpre  33319  lcfls1c  33607
  Copyright terms: Public domain W3C validator