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

Definition df-3an 939
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 937 . 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  941  3anrot  942  3ancoma  944  3anan32  949  3anor  951  3ioran  953  3simpa  955  3pm3.2i  1133  pm3.2an3  1134  3jca  1135  3anbi123i  1143  3imp  1148  3anbi123d  1255  3anim123d  1262  an6  1264  cadan  1402  19.26-3an  1607  nf3and  1848  nf3an  1853  hb3anOLD  1857  4exdistr  1939  eeeanv  1943  eeeanvOLD  1944  sb3an  2151  mopick2  2359  r19.26-3  2851  3reeanv  2887  ceqsex3v  3007  ceqsex4v  3008  ceqsex8v  3010  sbc3an  3235  elin3  3525  raltpg  3891  tpss  3996  dfopif  4013  disjxun  4245  otth2  4482  oteqex  4492  poirr  4559  po3nr  4562  wefrc  4621  dfwe2  4807  rabxp  4958  brinxp2  4983  brinxp  4984  f1orn  5735  dff1o6  6065  oprabid  6157  ndmovass  6289  elovmpt2  6345  dfxp3  6460  bropopvvv  6480  opiota  6589  oaord  6843  oeeui  6898  oeeu  6899  nnaord  6915  swoso  6989  fiint  7436  alephval3  8046  fpwwe2lem8  8567  fpwwe2lem9  8568  fpwwe2lem12  8571  ingru  8745  axgroth3  8761  ltrelxr  9194  ltxrlt  9201  wloglei  9614  sup2  10019  rexuz2  10583  ltxr  10770  elixx3g  10984  ixxun  10987  elioo4g  11026  elioopnf  11053  elioomnf  11054  elicopnf  11055  elxrge0  11063  elfz2  11105  elfzuzb  11108  fznn0  11168  uzsplit  11173  elfzo2  11198  fzolb2  11201  fzouzsplit  11223  fzind2  11253  abs2dif  12191  sinltx  12845  divalglem8  12975  divalglem10  12977  divalgb  12979  bitsval2  12992  rplpwr  13111  pythagtriplem2  13246  pythagtrip  13263  pwsle  13769  imasvscafn  13817  mreexmrid  13923  iscatd2  13961  issect  14034  issect2  14035  oppcsect  14054  isfunc  14116  funcpropd  14152  fucsect  14224  fucinv  14225  setcsect  14299  setcinv  14300  mndcl  14731  issubm2  14785  issubg3  14996  cycsubgcl  15002  eqgval  15025  eqger  15026  isgim  15085  gaorb  15120  gaorber  15121  gastacos  15123  galactghm  15142  ispgp  15262  efgcpbllema  15422  efgcpbllemb  15423  eqgabl  15490  dprdw  15604  rngpropd  15731  rngrghm  15748  isirred2  15842  drngid2  15887  islss  16047  islmim  16170  lmhmpropd  16181  isassa  16411  zndvds  16866  znleval  16871  znleval2  16872  obselocv  16991  isbasis3g  17050  leordtvallem2  17311  lmfval  17332  lmbr  17358  lmbr2  17359  lmmo  17480  dfcon2  17518  ptbasin  17645  ptbasfi  17649  txcnpi  17676  ptcnp  17690  hausdiag  17713  qtophmeo  17885  fbunfip  17937  elflim2  18032  hausflimi  18048  isfcls  18077  isfcls2  18081  istmd  18140  istgp  18143  istrg  18229  istdrg  18231  istdrg2  18243  istlm  18250  imasdsf1olem  18439  xmeterval  18498  xmeter  18499  prdsxmslem2  18595  blval2  18641  isngp  18679  isngp2  18680  isngp3  18681  isnlm  18747  cnbl0  18844  cnblcld  18845  elii1  18996  isphtpc  19055  phtpcer  19056  iscph  19169  lmmbr  19247  lmmbr2  19248  lmmbrf  19251  iscfil2  19255  iscau3  19267  iscau4  19268  iscauf  19269  caucfil  19272  isbn  19327  ishl2  19360  ovolfcl  19399  ioombl1lem4  19491  mbfmax  19575  iblpos  19718  limcrcl  19797  mpfrcl  19975  ig1pval3  20133  ulmdvlem3  20354  ellogdm  20566  fsumvma2  21034  chpchtsum  21039  chpub  21040  dchrelbas3  21058  nb3grapr2  21499  nb3gra2nb  21500  0wlk  21581  0trl  21582  constr2wlk  21634  3v3e3cycl1  21667  nvex  22126  isnv  22127  dfadj2  23424  cnvadj  23431  adjeq  23474  eleigvec  23496  eleigvec2  23497  chirredi  23933  or3di  23987  eliccelico  24212  omndmul2  24317  isorng  24432  relogbcl  24632  eulerpartlemv  24906  eulerpartlemd  24908  eulerpartlemn  24923  prob01  24931  probun  24937  pconcon  25178  rescon  25193  iscvm  25206  cvmlift2lem12  25261  cvmlift3lem5  25270  lediv2aALT  25377  dfso3  25437  divelunit  25445  br6  25640  preduz  25735  nofulllem2  25918  nofulllem5  25921  elfuns  26020  brimg  26042  brsuccf  26046  axeuclidlem  26161  axeuclid  26162  cgrxfr  26249  segcon2  26299  seglecgr12im  26304  seglecgr12  26305  segletr  26308  btwnoutside  26319  broutsideof3  26320  outsideoftr  26323  outsidele  26326  fdc  26716  isbnd3b  26761  ablo4pnp  26822  crngm4  26880  isidlc  26892  pridl  26914  ispridl2  26915  ispridlc  26947  ts3an1  26999  ts3an2  27000  ts3an3  27001  3anrabdioph  27178  issdrg2  27818  fgraphxp  27842  rfcnnnub  28017  stoweidlem35  28094  ndmaovass  28381  3an4anass  28384  rexdifpr  28394  otthg  28400  oprabv  28423  elovmpt2rab  28424  elovmpt2rab1  28425  elfz2z  28448  elfzmlbp  28450  ccatsymb  28531  swrdccatin2  28564  swrdccatin12lem3  28566  swrdccatin12lem4  28567  swrdccatin12  28568  cshweqdif2s  28625  usgra2pth0  28670  el2wlkonotot0  28724  el2wlkonotot  28725  el2wlkonotot1  28726  2wlkonotv  28729  usg2spthonot0  28741  cusgraisrusgra  28769  frgra3v  28786  1to3vfriswmgra  28791  ex3  29053  dfvd3  29078  3impexpVD  29365  bnj170  29459  bnj248  29461  bnj252  29464  bnj253  29465  bnj945  29541  bnj1098  29551  bnj1224  29570  bnj150  29644  bnj153  29648  bnj545  29663  bnj557  29669  bnj571  29674  bnj594  29680  bnj864  29690  bnj865  29691  bnj849  29693  bnj964  29711  bnj986  29722  bnj996  29723  bnj1033  29735  bnj1110  29748  bnj1128  29756  bnj1174  29769  sb3anNEW7  30037  eeeanvOLD7  30101  islshpsm  30174  islshpat  30211  cmtfvalN  30404  cmtvalN  30405  ishlat1  30546  ishlat2  30547  3dim0  30650  2dim  30663  islvol5  30772  lhpexle3  31205  cdleme0ex2N  31417  cdleme0nex  31483  cdlemg2cex  31784  cdlemg33b0  31894  cdlemg33b  31900  cdlemg33c  31901  cdlemg33e  31903  dib1dim  32359  diblsmopel  32365  dihopelvalcpre  32442  lcfls1c  32730
  Copyright terms: Public domain W3C validator