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  1411  cadanOLD  1412  19.26-3an  1623  nf3and  1848  nf3an  1853  hb3anOLD  1857  4exdistr  1938  eeeanv  1942  eeeanvOLD  1943  sb3an  2150  mopick2  2400  r19.26-3  2894  3reeanv  2932  ceqsex3v  3053  ceqsex4v  3054  ceqsex8v  3056  sbc3an  3286  elin3  3578  raltpg  3959  tpss  4064  dfopif  4082  disjxun  4316  otth2  4596  oteqex  4606  poirr  4673  po3nr  4676  wefrc  4735  rabxp  4897  brinxp2  4922  brinxp  4923  f1orn  5668  dff1o6  5994  oprabid  6127  ndmovass  6261  elovmpt2  6317  dfwe2  6403  opiota  6639  dfxp3  6640  bropopvvv  6659  oaord  6952  oeeui  7007  oeeu  7008  nnaord  7024  swoso  7098  fiint  7549  alephval3  8162  fpwwe2lem8  8683  fpwwe2lem9  8684  fpwwe2lem12  8687  ingru  8861  axgroth3  8877  ltrelxr  9317  ltxrlt  9324  wloglei  9745  sup2  10152  rexuz2  10770  ltxr  10959  elixx3g  11177  ixxun  11180  elioo4g  11219  elioopnf  11246  elioomnf  11247  elicopnf  11248  elxrge0  11256  elfz2  11300  elfzuzb  11303  elfzmlbp  11347  fznn0  11376  uzsplit  11382  elfzo2  11408  fzolb2  11411  fzouzsplit  11436  ssfzo12bi  11471  fzind2  11486  ccatsymb  12128  swrdccatin2  12225  swrdccatin12lem2  12227  swrdccatin12lem3  12228  swrdccatin12  12229  repsdf2  12263  repswsymball  12264  repswsymballbi  12265  repswswrd  12269  abs2dif  12667  sinltx  13320  divalglem8  13451  divalglem10  13453  divalgb  13455  bitsval2  13468  rplpwr  13587  pythagtriplem2  13731  pythagtrip  13748  pwsle  14268  imasvscafn  14316  mreexmrid  14422  iscatd2  14460  issect  14533  issect2  14534  oppcsect  14553  isfunc  14615  funcpropd  14651  fucsect  14723  fucinv  14724  setcsect  14798  setcinv  14799  mndcl  15261  issubm2  15315  issubg3  15531  cycsubgcl  15537  eqgval  15560  eqger  15561  isgim  15620  gaorb  15655  gaorber  15656  gastacos  15658  symg2bas  15684  galactghm  15689  gsmsymgreqlem2  15712  ispgp  15835  efgcpbllema  15995  efgcpbllemb  15996  eqgabl  16063  dprdw  16183  rngpropd  16310  rngrghm  16327  isirred2  16422  drngid2  16467  islss  16630  islmim  16757  lmhmpropd  16768  isassa  17000  zndvds  17455  znleval  17460  znleval2  17461  obselocv  17580  mdetunilem7  17896  isbasis3g  18028  leordtvallem2  18289  lmfval  18310  lmbr  18336  lmbr2  18337  lmmo  18458  dfcon2  18497  ptbasin  18624  ptbasfi  18628  txcnpi  18655  ptcnp  18669  hausdiag  18692  qtophmeo  18864  fbunfip  18916  elflim2  19011  hausflimi  19027  isfcls  19056  isfcls2  19060  istmd  19119  istgp  19122  istrg  19208  istdrg  19210  istdrg2  19222  istlm  19229  imasdsf1olem  19418  xmeterval  19477  xmeter  19478  prdsxmslem2  19574  blval2  19620  isngp  19658  isngp2  19659  isngp3  19660  isnlm  19726  cnbl0  19823  cnblcld  19824  elii1  19975  isphtpc  20034  phtpcer  20035  iscph  20148  lmmbr  20226  lmmbr2  20227  lmmbrf  20230  iscfil2  20234  iscau3  20246  iscau4  20247  iscauf  20248  caucfil  20251  isbn  20306  ishl2  20339  ovolfcl  20378  ioombl1lem4  20470  mbfmax  20554  iblpos  20697  limcrcl  20776  mpfrcl  20954  ig1pval3  21112  ulmdvlem3  21333  ellogdm  21550  fsumvma2  22019  chpchtsum  22024  chpub  22025  dchrelbas3  22043  nb3grapr2  22484  nb3gra2nb  22485  0wlk  22566  0trl  22567  constr2wlk  22619  3v3e3cycl1  22652  nvex  23111  isnv  23112  dfadj2  24411  cnvadj  24418  adjeq  24461  eleigvec  24483  eleigvec2  24484  chirredi  24920  or3di  24974  eliccelico  25197  omndmul2  25307  isorng  25428  relogbcl  25641  eulerpartlemv  25921  eulerpartlemd  25923  eulerpartlemn  25938  prob01  25946  probun  25952  pconcon  26266  rescon  26281  iscvm  26294  cvmlift2lem12  26349  cvmlift3lem5  26358  lediv2aALT  26462  dfso3  26516  divelunit  26524  br6  26719  preduz  26814  nofulllem2  26997  nofulllem5  27000  elfuns  27099  brimg  27121  brsuccf  27125  axeuclidlem  27240  axeuclid  27241  cgrxfr  27328  segcon2  27378  seglecgr12im  27383  seglecgr12  27384  segletr  27387  btwnoutside  27398  broutsideof3  27399  outsideoftr  27402  outsidele  27405  fdc  27821  isbnd3b  27866  ablo4pnp  27927  crngm4  27985  isidlc  27997  pridl  28019  ispridl2  28020  ispridlc  28052  ts3an1  28104  ts3an2  28105  ts3an3  28106  3anrabdioph  28269  issdrg2  28737  fgraphxp  28761  rfcnnnub  28933  stoweidlem35  29009  ndmaovass  29291  3an4anass  29294  rexdifpr  29305  otthg  29311  oprabv  29338  elovmpt2rab  29339  elovmpt2rab1  29340  elfz2z  29377  usgra2pth0  29483  wwlknred  29536  wwlknndef  29550  el2wlkonotot0  29572  el2wlkonotot  29573  el2wlkonotot1  29574  2wlkonotv  29577  usg2spthonot0  29589  isclwlk  29602  clwwlkprop  29614  clwwlknndef  29617  clwwlknwwlkncl  29643  wwlkext2clwwlk  29646  wwlksubclwwlk  29647  clwwnisshclwwn  29654  erclwwlkref  29664  erclwwlknref  29680  clwlkfoclwwlk  29699  cusgraisrusgra  29732  rusgranumwlkl1  29740  rusgranumwlkb0  29752  rusgra0edg  29754  rusgranumwlk  29756  frgra3v  29775  1to3vfriswmgra  29780  frgraregorufrg  29846  extwwlkfablem2  29852  numclwwlkffin  29856  numclwwlkovfel2  29857  numclwwlkovf2  29858  numclwwlkovf2ex  29860  numclwwlkovgelim  29863  numclwlk1lem2fo  29869  numclwwlk2lem1  29876  numclwwlk7  29888  ex3  30126  dfvd3  30151  3impexpVD  30438  bnj170  30532  bnj248  30534  bnj252  30537  bnj253  30538  bnj945  30614  bnj1098  30624  bnj1224  30643  bnj150  30717  bnj153  30721  bnj545  30736  bnj557  30742  bnj571  30747  bnj594  30753  bnj864  30763  bnj865  30764  bnj849  30766  bnj964  30784  bnj986  30795  bnj996  30796  bnj1033  30808  bnj1110  30821  bnj1128  30829  bnj1174  30842  sb3anNEW11  31191  eeeanvOLD11  31255  islshpsm  31328  islshpat  31365  cmtfvalN  31558  cmtvalN  31559  ishlat1  31700  ishlat2  31701  3dim0  31804  2dim  31817  islvol5  31926  lhpexle3  32359  cdleme0ex2N  32571  cdleme0nex  32637  cdlemg2cex  32938  cdlemg33b0  33048  cdlemg33b  33054  cdlemg33c  33055  cdlemg33e  33057  dib1dim  33513  diblsmopel  33519  dihopelvalcpre  33596  lcfls1c  33884
  Copyright terms: Public domain W3C validator