Axiom ax-mp 5

Description: Rule of Modus Ponens. The postulated inference rule of propositional calculus. See, e.g., Rule 1 of [Hamilton] p. 73. The rule says, "if ph is true, and ph implies ps, then ps must also be true". This rule is sometimes called "detachment", since it detaches the minor premise from the major premise. "Modus ponens" is short for "modus ponendo ponens", a Latin phrase that means "the mode that by affirming affirms" - remark in [Sanford] p. 39. This rule is similar to the rule of modus tollens mto 666.

Note: In some web page displays such as the Statement List, the symbols "& " and "=> " informally indicate the relationship between the hypotheses and the assertion (conclusion), abbreviating the English words "and" and "implies". They are not part of the formal language. (Contributed by NM, 30-Sep-1992.)

Hypotheses

Ref	Expression
min	|- ph
maj	|- ( ph -> ps )

Assertion

Ref	Expression
ax-mp	|- ps

Detailed syntax breakdown of Axiom ax-mp

Step	Hyp	Ref	Expression
1		wps	1 wff ps

This axiom is referenced by:  mp2b  8  a1i  9  mp1i  10  a2i  11  mpd  13  mp2  16  idALT  20  simpli  111  simpri  113  biimpi  120  bicomi  132  mpbi  145  mpbir  146  imbi1i  238  a1bi  243  tbt  247  biantru  302  biantrur  303  mp2an  426  pm2.65i  642  notnoti  648  pm2.21i  649  pm2.24ii  650  notbii  672  nbn  704  ori  728  orci  736  olci  737  biorfi  751  imorri  754  dcbii  845  simp1i  1030  simp2i  1031  simp3i  1032  3mix1i  1193  3mix2i  1194  3mix3i  1195  3jaoi  1337  mptru  1404  dfnot  1413  mptnan  1465  mtpor  1467  mtpxor  1468  dcfromnotnotr  1490  dcfromcon  1491  dcfrompeirce  1492  mpg  1497  19.23h  1544  hbequid  1559  axi12  1560  nfri  1565  spi  1582  19.21  1629  eximii  1648  19.35i  1671  nfn  1704  19.37aiv  1721  19.23  1724  exan  1739  equid  1747  hbae  1764  equvini  1804  equveli  1805  sbid  1820  sbieh  1836  exdistrfor  1846  dveeq2or  1862  ax11v  1873  ax11ev  1874  equs5or  1876  sb4or  1879  sb4bor  1881  nfsb2or  1883  sbequilem  1884  sbequi  1885  speiv  1908  nfsbxy  1993  nfsbxyt  1994  sbco  2019  sbcocom  2021  sbcomxyyz  2023  sbal1yz  2052  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  eumoi  2110  moani  2148  elsb1  2207  elsb2  2208  eqeq1i  2237  eqeq2i  2240  eleq1i  2295  eleq2i  2296  nfcrii  2365  neeq1i  2415  neeq2i  2416  necon3i  2448  rspec  2582  rgen2a  2584  mprg  2587  r19.21  2606  r19.23  2639  raleqi  2732  rexeqi  2733  rabeqif  2791  elv  2804  elexi  2813  ceqsal  2830  vtocl3  2858  vtoclef  2877  vtocle  2878  spcv  2898  spcev  2899  clel3  2939  elabf  2947  elab2  2952  elab3  2956  euxfrdc  2990  reueq  3003  rmoimi2  3007  sbsbc  3033  sbc8g  3037  sbc6  3055  sbcie  3064  sbcrex  3109  csbvarg  3153  csbief  3170  csbie2  3175  sbnfc2  3186  sseli  3221  sselii  3222  sseq1i  3251  sseq2i  3252  difeq1i  3319  difeq2i  3320  uneq1i  3355  uneq2i  3356  ineq1i  3402  ineq2i  3403  ssinss1  3434  difdif2ss  3462  n0ii  3501  ne0ii  3502  vn0  3503  vn0m  3504  abf  3536  disj2  3548  difid  3561  0dif  3564  disjdif  3565  difin0  3566  undif1ss  3567  difdifdirss  3577  iftruei  3609  iffalsei  3612  ifbieq2i  3627  ifbieq12i  3629  pweqi  3654  pwid  3665  sneqi  3679  elsn  3683  elpr  3688  elsn2  3701  ralsn  3710  rexsn  3711  eltp  3715  rabrsndc  3735  preq1i  3747  preq2i  3748  prid1  3773  snnz  3787  snm  3788  prnz  3791  prm  3792  tpnz  3794  snss  3804  snsssn  3840  opeq1i  3861  opeq2i  3862  unieqi  3899  unissi  3912  inteqi  3928  intmin2  3950  intab  3953  intsn  3959  iinconstm  3975  iuniin  3976  iinss1  3978  iunxdif2  4015  ssiinf  4016  iinss  4018  iinss2  4019  iinab  4028  iundif2ss  4032  iindif2m  4034  iinin2m  4035  iunxsn  4043  iunxprg  4047  iinpw  4057  invdisjrab  4078  sndisj  4080  disjxsn  4082  breqi  4090  breq1i  4091  breq2i  4092  brab1  4132  opabbii  4152  truni  4197  bm1.3ii  4206  a9evsep  4207  ax9vsep  4208  zfnuleu  4209  axnul  4210  ssexi  4223  rabex  4230  rabex2  4232  elpw2  4243  pwnss  4245  iin0r  4255  intv  4256  pwex  4269  snex  4271  notnotsnex  4273  ord3ex  4276  dtruarb  4277  undifexmid  4279  intid  4312  opnzi  4323  copsexg  4332  opwo0id  4337  opelopabf  4365  epelc  4384  elon  4467  inton  4486  onn0  4493  onm  4494  elsuc  4499  elsuc2  4500  sucid  4510  iunsuc  4513  onordi  4519  ontrci  4520  onelssi  4522  eusvnf  4546  ssonunii  4583  sucex  4593  onssi  4609  onsuci  4610  ordtriexmidlem  4613  ordtriexmidlem2  4614  ordtriexmid  4615  ontriexmidim  4616  ordtri2orexmid  4617  2ordpr  4618  ontr2exmid  4619  onsucsssucexmid  4621  onsucelsucexmid  4624  regexmidlemm  4626  reg2exmid  4630  onirri  4637  ruALT  4645  onprc  4646  sucon  4647  dtru  4654  0elsucexmid  4659  ordpwsucexmid  4664  ordtri2or2exmid  4665  ontri2orexmidim  4666  dcextest  4675  omex  4687  find  4693  omelon  4703  nnoni  4705  limom  4708  nnregexmid  4715  omsinds  4716  xpeq1i  4741  xpeq2i  4742  0nelxp  4749  opthprc  4773  mosubop  4788  releqi  4805  relssi  4813  relin1  4841  relin2  4842  reldif  4843  inopab  4858  difopab  4859  xpiindim  4863  opabbi2dv  4875  ideq  4878  coeq1i  4885  coeq2i  4886  cnveqi  4901  eldm  4924  eldm2  4925  dmeqi  4928  dmv  4943  rneqi  4956  elrnmpti  4981  dmex  4995  rnex  4996  reseq1i  5005  reseq2i  5006  residm  5041  resex  5050  resmpt3  5058  imaeq1i  5069  imaeq2i  5070  elima  5077  imaex  5087  elimasn  5099  args  5101  epini  5103  dfse2  5105  eliniseg2  5112  relbrcnv  5113  cotr  5114  issref  5115  cnvsym  5116  asymref  5118  intirr  5119  codir  5121  qfto  5122  ssrnres  5175  cnveq0  5189  cnvsn0  5201  dmsnop  5206  rnsnop  5213  resdm2  5223  dfco2a  5233  cocnvcnv1  5243  coi2  5249  coires1  5250  cnvssrndm  5254  cossxp  5255  cocnvres  5257  relrelss  5259  relcoi2  5263  unidmrn  5265  dfdm2  5267  unixpm  5268  cnvexg  5270  cnvex  5271  cnviinm  5274  iotaval  5294  funeqi  5343  funi  5354  funres  5363  funcnvsn  5370  funcnvcnv  5384  funin  5396  funcnvres  5398  isarep2  5412  fneq1i  5419  fneq2i  5420  fndmi  5425  fnresdisj  5437  fnresi  5445  mpt0  5455  dmmpti  5457  feq1i  5470  feq2i  5471  fdmi  5485  fun2  5504  fssres  5507  resasplitss  5511  fintm  5517  fconst6  5531  f1ores  5593  foimacnv  5596  resdif  5600  funcocnv2  5603  f10d  5613  f1ovi  5618  fveq1i  5634  fveq2i  5636  0fv  5671  fvun1  5706  fvopab3ig  5714  fvmptss2  5715  mptrcl  5723  elfvmptrab1  5735  fndmdif  5746  fneqeql2  5750  f1oresrab  5806  fmptco  5807  funopsn  5823  fnressn  5833  fressnfv  5834  fmptap  5837  fvsnun1  5844  fvsnun2  5845  fsnunfv  5848  fconst2  5864  mptex  5873  fnfvimad  5883  riotabiia  5983  acexmidlema  6002  acexmidlemb  6003  acexmidlemcase  6006  acexmidlem2  6008  acexmidlemv  6009  oveq1i  6021  oveq2i  6022  oveqi  6024  oprabidlem  6042  0neqopab  6059  oprabbii  6069  oprabss  6100  mpompt  6106  funoprab  6114  fnoprab  6117  ovigg  6135  elmpocl  6210  relmptopab  6217  resfunexgALT  6263  cofunexg  6264  mptexw  6268  opabex3d  6276  opabex3  6277  1st0  6300  2nd0  6301  op1st  6302  op2nd  6303  f1stres  6315  f2ndres  6316  fo1stresm  6317  fo2ndresm  6318  1stcof  6319  2ndcof  6320  1stexg  6323  2ndexg  6324  releldm2  6341  reldm  6342  dfoprab3  6347  mpomptsx  6355  mpompts  6356  fnmpoi  6361  dmmpo  6362  mpoexxg  6368  mpoexw  6371  1stconst  6379  2ndconst  6380  dfmpo  6381  algrflem  6387  algrflemg  6388  cnvoprab  6392  f1od2  6393  elmpom  6396  mpoxopn0yelv  6398  mpoxopoveq  6399  tposssxp  6408  brtpos2  6410  reldmtpos  6412  dftpos2  6420  dftpos4  6422  tpostpos  6423  tpostpos2  6424  tposfo  6430  tposf  6431  tposeqi  6436  tposex  6437  tposoprab  6439  issmo  6447  smores  6451  smores2  6453  iordsmo  6456  smo0  6457  tfrlem8  6477  tfrexlem  6493  tfr1onlem3  6497  tfr1onlemsucaccv  6500  tfr1onlembxssdm  6502  tfr1onlemres  6508  tfri1dALT  6510  tfri2  6525  rdgisuc1  6543  rdg0  6546  frecfun  6554  frec0g  6556  freccllem  6561  frecfcllem  6563  frecsuclem  6565  frecrdg  6567  2on0  6585  xp01disj  6594  2oconcl  6600  fnoa  6608  oaexg  6609  fnom  6611  omexg  6612  fnoei  6613  oeiexg  6614  oei0  6620  oacl  6621  oasuc  6625  o1p1e2  6629  omsuc  6633  nna0r  6639  nnm0r  6640  1onn  6681  2onn  6682  3onn  6683  4onn  6684  2ssom  6685  eqerlem  6726  eceq2i  6733  elqs  6748  qsex  6754  ecqs  6759  iinerm  6769  th3qlem1  6799  th3q  6802  mapsn  6852  mapsnf1o3  6859  ixpiinm  6886  ixpssmap  6894  brdom  6914  f1dom  6926  enref  6931  dom2  6941  idssen  6943  ssdomg  6945  ensymi  6949  ensn1  6963  fiprc  6983  1domsn  6994  dom1o  6995  xpcomf1o  7002  xpcomco  7003  dom0  7017  0dom  7018  xpmapenlem  7028  phplem2  7032  php5  7037  snnen2og  7038  1nen2  7040  php5dom  7042  ssfilem  7055  ssfiexmid  7056  domfiexmid  7058  0fi  7064  diffitest  7067  findcard  7068  findcard2  7069  findcard2s  7070  isinfinf  7077  ac6sfi  7078  inffiexmid  7089  pw1fin  7093  unfiexmid  7101  xpfi  7115  fisseneq  7117  ssfirab  7119  residfi  7128  en1eqsn  7136  snexxph  7138  sbthlem2  7146  sbthlemi3  7147  sbthlemi6  7150  sbthlem7  7151  fi0  7163  supeq1i  7176  infeq1i  7201  djuexb  7232  djuf1olemr  7242  inresflem  7248  djuinr  7251  updjudhcoinlf  7268  updjudhcoinrg  7269  casefun  7273  caserel  7275  caseinj  7277  caseinl  7279  caseinr  7280  omp1eomlem  7282  endjusym  7284  difinfsn  7288  difinfinf  7289  djuinj  7294  0ct  7295  ctmlemr  7296  ctssdclemn0  7298  ctssdccl  7299  omct  7305  ctfoex  7306  finomni  7328  exmidomni  7330  fodjuomni  7337  ctssexmid  7338  fodjumkv  7348  nninfwlporlem  7361  nninfwlpoimlemg  7363  nninfwlpoim  7367  nninfinfwlpo  7368  card0  7381  ficardon  7382  exmidonfinlem  7392  dju1p1e2  7396  exmidfodomrlemim  7400  exmidfodomrlemr  7401  exmidfodomrlemrALT  7402  iftrueb01  7429  3nelsucpw1  7440  sucpw1nss3  7441  3nsssucpw1  7442  2onetap  7462  exmidmotap  7468  0npi  7521  dmaddpi  7533  dmmulpi  7534  1lt2pi  7548  0nnq  7572  1nq  7574  dmaddpq  7587  dmmulpq  7588  rec1nq  7603  1lt2nq  7614  halfnqq  7618  prarloclemarch2  7627  enq0enq  7639  nqnq0pi  7646  nnnq0lem1  7654  addnnnq0  7657  mulnnnq0  7658  nq0m0r  7664  addpinq1  7672  prarloclem5  7708  prarloclemcalc  7710  1pr  7762  1idprl  7798  1idpru  7799  ltexprlemm  7808  recexprlem1ssl  7841  recexprlem1ssu  7842  suplocexprlemell  7921  suplocexprlem2b  7922  suplocexprlemmu  7926  suplocexprlemdisj  7928  suplocexprlemloc  7929  suplocexprlemub  7931  suplocexprlemlub  7932  prsrlem1  7950  addsrpr  7953  mulsrpr  7954  gt0srpr  7956  0nsr  7957  0r  7958  1sr  7959  m1r  7960  m1m1sr  7969  caucvgsr  8010  suplocsrlempr  8015  addresr  8045  mulresr  8046  pitonnlem1  8053  peano1nnnn  8060  axi2m1  8083  axcnre  8089  peano5nnnn  8100  axcaucvg  8108  mpomulf  8157  mulridi  8169  mullidi  8170  pnfnre  8209  mnfnre  8210  pnfnemnf  8222  mnfxr  8224  rexri  8225  ltnri  8260  ltleii  8270  00id  8308  addridi  8309  addlidi  8310  0cnALT  8357  negeqi  8361  negicn  8368  neg0  8413  renegcli  8429  negcli  8435  negidi  8436  negnegi  8437  subidi  8438  subid1i  8439  negne0bi  8440  negrebi  8441  mul02i  8557  mul01i  8558  mulm1i  8570  leidi  8653  gt0ne0ii  8655  inelr  8752  msqge0i  8785  gt0ap0ii  8796  1div1e1  8872  div1i  8908  eqnegi  8909  recclapi  8910  recidapi  8911  divmulapi  8934  rerecclapi  8945  redivclapi  8947  rerecapb  9011  recgt0  9018  ltp1i  9073  divgt0ii  9087  ltmul1ii  9096  ltdiv1ii  9097  sup3exmid  9125  peano5nni  9134  nnrei  9140  1nn  9142  nngt0i  9161  neg1ap0  9240  2timesi  9261  times2i  9262  2nn  9293  3nn  9294  4nn  9295  5nn  9296  6nn  9297  7nn  9298  8nn  9299  9nn  9300  2muline0  9357  rehalfcli  9381  nn0ssre  9394  nnnn0i  9398  dfn2  9403  0nn0  9405  nn0ge0i  9417  zrei  9473  neg1z  9499  nn0negzi  9502  dfz2  9540  nneoi  9572  peano5uzi  9577  dfuzi  9578  nn0ind-raph  9585  deceq1i  9605  deceq2i  9606  10nn  9614  numltc  9624  eluzel2  9748  eluz1i  9751  nn0uz  9779  nnuz  9780  uzuzle35  9787  infrenegsupex  9816  lbzbi  9838  divfnzn  9843  qdivcl  9865  irrmul  9869  irrmulap  9870  cnref1o  9873  0ltpnf  10005  mnflt0  10007  0lepnf  10013  xrltnsym  10016  xrlttri3  10020  nltpnft  10037  ngtmnft  10040  xrrebnd  10042  xnegmnf  10052  xneg0  10054  xltnegi  10058  xaddmnf1  10071  xaddmnf2  10072  mnfaddpnf  10074  xaddid1  10085  xnn0lenn0nn0  10088  xnn0xadd0  10090  xposdif  10105  ixxex  10122  iooval2  10138  unirnioo  10196  ioorebasg  10198  elrege0  10199  fzval2  10234  fzen  10266  fzprval  10305  fztpval  10306  uzdisj  10316  ige2m1fz  10333  fz01or  10334  fz1ssfz0  10340  fz0sn  10344  fz0tp  10345  fz0to3un2pr  10346  fz0to4untppr  10347  nn0disj  10361  1fv  10362  4fvwrd4  10363  fzo0ss1  10399  fzo01  10449  fzo12sn  10450  fzo0to2pr  10451  fzo0to3tp  10452  fzo0to42pr  10453  zsupssdc  10486  qbtwnxr  10505  flval  10520  fldiv4lem1div2  10555  modqfrac  10587  modqmulnn  10592  q2txmodxeq0  10634  frecuzrdgdom  10668  frecuzrdgfun  10670  frecuzrdgsuct  10674  frechashgf1o  10678  nnct  10685  xnn0nnen  10687  fxnn0nninf  10689  0tonninf  10690  1tonninf  10691  iseqvalcbv  10709  ser0f  10784  0exp0e1  10794  qexpcl  10805  qexpclz  10810  m1expcl2  10811  1exp  10818  sqvali  10869  sqcli  10870  sqeq0i  10871  resqcli  10874  sq1  10883  neg1sqe1  10884  iexpcyc  10894  qsqeqor  10900  facnn  10977  fac0  10978  fac1  10979  fac2  10981  fac3  10982  fac4  10983  bcval  10999  bcm1k  11010  bcpasc  11016  bccl  11017  4bc3eq4  11023  4bc2eq6  11024  hashinfom  11028  hashennn  11030  hashfz1  11033  fihasheq0  11043  hash0  11046  hashsng  11048  fihashen1  11049  omgadd  11052  hashp1i  11061  hashxp  11077  fimaxq  11078  zfz1iso  11092  hash2en  11094  wrdexi  11113  wrdv  11116  wrdeqi  11123  wrd0  11125  lsw0  11148  ccatclab  11158  ccatidid  11174  s1prc  11187  ccat1st1st  11205  swrds1  11236  fnpfx  11245  swrdccatin2  11297  pfxccatin12lem2  11299  cats1fvn  11332  shftidt2  11380  cjexp  11441  re0  11443  im0  11444  re1  11445  im1  11446  cj0  11449  cji  11450  recli  11459  imcli  11460  cjcli  11461  replimi  11462  cjcji  11463  reim0bi  11464  rerebi  11465  cjrebi  11466  recji  11467  imcji  11468  cjmulrcli  11469  cjmulvali  11470  cjmulge0i  11471  renegi  11472  imnegi  11473  cjnegi  11474  addcji  11475  uzin2  11535  rexanuz  11536  rexfiuz  11537  sqrtrval  11548  sqrt0  11552  resqrexlemcalc3  11564  resqrexlemcvg  11567  resqrex  11574  abs0  11606  absi  11607  qabsor  11623  absimle  11632  recan  11657  caubnd2  11665  leabsi  11676  absrei  11677  sqrtpclii  11678  sqrtgt0ii  11679  absvalsqi  11688  absvalsq2i  11689  abscli  11690  absge0i  11691  absval2i  11692  abs00i  11693  absgt0api  11694  absnegi  11695  abscji  11696  releabsi  11697  infxrnegsupex  11811  xrbdtri  11824  cbvsum  11908  sumeq1i  11911  sum0  11936  isumz  11937  fisumss  11940  fsumsersdc  11943  fsumadd  11954  isumclim  11969  isumclim3  11971  fsumcnv  11985  modfsummodlem1  12004  fsumrelem  12019  binomlem  12031  binom  12032  arisum2  12047  expcnv  12052  0.999...  12069  prodf1f  12091  cbvprod  12106  prodeq1i  12109  zproddc  12127  zprodap0  12129  prod0  12133  fprodssdc  12138  prodsnf  12140  fprodcnv  12173  fprodge0  12185  fprodge1  12187  ef0lem  12208  esum  12210  ere  12218  ege2le3  12219  ef0  12220  eff2  12228  efsep  12239  reeff1  12248  sin0  12277  cos0  12278  ef01bndlem  12304  cos2bnd  12308  sincos1sgn  12313  sincos2sgn  12314  sin4lt0  12315  eirr  12327  0dvds  12359  dvds1  12401  z0even  12459  n2dvdsm1  12461  z2even  12462  n2dvds3  12463  ndvdssub  12478  ndvdsi  12481  flodddiv4  12484  bits0  12496  bitsfzo  12503  0bits  12507  m1bits  12508  bitsinv1lem  12509  bitsinv1  12510  gcddvds  12521  gcd1  12545  6gcd4e2  12553  bezoutlembi  12563  dfgcd3  12568  dfgcd2  12572  nninfctlemfo  12598  nninfct  12599  3lcm2e6woprm  12645  qredeu  12656  isprm2lem  12675  isprm3  12677  prm2orodd  12685  isprm5lem  12700  sqrt2irr0  12723  pw2dvds  12725  phicl2  12773  phi1  12778  dfphi2  12779  phiprmpw  12781  eulerthlemrprm  12788  eulerthlemh  12790  odzval  12801  oddprm  12819  pczpre  12857  pcdiv  12862  pc0  12864  pcqdiv  12867  pcrec  12868  pcexp  12869  pcxcl  12871  pcxqcl  12872  pcdvdstr  12887  pc2dvds  12890  dvdsprmpweqnn  12896  pcmpt  12903  qexpz  12912  pockthi  12918  1arith2  12928  4sqlemffi  12956  4sqlem11  12961  4sqlem13m  12963  4sqlem19  12969  dec2dvds  12971  dec5nprm  12974  modxai  12976  modxp1i  12978  numexp0  12982  numexp1  12983  ennnfonelemp1  13014  ennnfonelem1  13015  ennnfonelemkh  13020  ennnfonelemex  13022  ennnfonelemnn0  13030  ennnfonelemr  13031  exmidunben  13034  ctinfomlemom  13035  ctinfom  13036  ctinf  13038  qnnen  13039  omctfn  13051  omiunct  13052  ssnnctlemct  13054  nninfdc  13061  structcnvcnv  13085  structfun  13087  structfn  13088  ndxarg  13092  ndxid  13093  setsresg  13107  setsslnid  13121  basmex  13129  basmexd  13130  strleun  13174  strle1g  13176  prdsex  13339  prdsvallem  13342  prdsval  13343  prdsbaslemss  13344  imasaddfnlemg  13384  quslem  13394  xpsfrnel  13414  xpsff1o  13419  ismgmn0  13428  fn0g  13445  0g0  13446  fngsum  13458  idghm  13833  rhmfn  14173  rmodislmodlem  14351  rmodislmod  14352  lidlmex  14476  mopnset  14553  cntopex  14555  cnfldex  14560  cnfldbas  14561  mpocnfldadd  14562  mpocnfldmul  14564  cnfldcj  14566  cnfldtset  14567  cnfldle  14568  cnfldds  14569  cnring  14571  cnfld0  14572  cnfld1  14573  cnfldneg  14574  cnfldplusf  14575  cnfldsub  14576  cnfldmulg  14577  cnfldexp  14578  cnsubglem  14580  cnsubrglem  14581  gzsubrg  14583  gsumfzfsumlem0  14587  cnfldui  14590  zringring  14594  zringabl  14595  zringgrp  14596  zring1  14602  zringsubgval  14606  expghmap  14608  znval  14637  znle  14638  znbaslemnn  14640  znbas  14645  znzrh2  14647  znzrhval  14648  znzrhfo  14649  znleval  14654  znidom  14658  znidomb  14659  fnpsr  14668  psrelbas  14676  psradd  14680  psraddcl  14681  psr1clfi  14689  mplrcl  14695  mplbasss  14697  mpladd  14705  istopon  14724  topontopi  14727  toponunii  14728  toponrestid  14732  istps  14743  topontopn  14748  eltpsi  14752  eltg4i  14766  eltg3  14768  tg1  14770  tg2  14771  tgclb  14776  topnex  14797  sn0topon  14799  distps  14802  cldrcl  14813  sn0cld  14848  restco  14885  lmrcl  14903  ssidcn  14921  cnconst2  14944  cnptopresti  14949  cnptoprest  14950  txuni2  14967  txbas  14969  eltx  14970  txcnp  14982  upxp  14983  txcnmpt  14984  uptx  14985  txcn  14986  txrest  14987  txlm  14990  cnmptid  14992  cnmpt1st  14999  cnmpt2nd  15000  hmeofn  15013  psmetge0  15042  ismeti  15057  xmetunirn  15069  xmetge0  15076  unirnblps  15133  unirnbl  15134  mopnex  15216  qtopbasss  15232  retop  15235  uniretop  15236  iooretopg  15239  cnxmet  15242  cntoptopon  15243  cnbl0  15245  cnfldxms  15248  cnfldtps  15249  rexmet  15260  blssioo  15264  tgioo  15265  tgqioo  15266  cnopnap  15322  hovercncf  15357  limcresi  15377  dvfvalap  15392  dvidlemap  15402  dvidrelem  15403  dvidsslem  15404  dvcnp2cntop  15410  dvcoapbr  15418  dvexp2  15423  dvrecap  15424  dveflem  15437  dvef  15438  plyun0  15447  plyrecj  15474  dvply2  15478  reeff1o  15484  sin0pilem1  15492  sin0pilem2  15493  pilem3  15494  pigt2lt4  15495  pire  15497  sinhalfpilem  15502  pidiv2halves  15506  cosneghalfpi  15509  cospi  15511  efipi  15512  sin2pi  15514  cos2pi  15515  ef2pi  15516  cosq14gt0  15543  coseq00topi  15546  coseq0negpitopi  15547  sincos4thpi  15551  sincos6thpi  15553  sincos3rdpi  15554  pigt3  15555  cos02pilt1  15562  ioocosf1o  15565  dfrelog  15571  relogf1o  15572  relogcl  15573  relogiso  15584  rpcxpsqrt  15633  rpabscxpbnd  15651  2logb9irr  15682  2logb9irrALT  15685  sqrt2cxp2logb9e3  15686  2irrexpq  15687  2logb9irrap  15688  2irrexpqap  15689  mpodvdsmulf1o  15701  fsumdvdsmul  15702  perfectlem2  15711  lgsdir2lem1  15744  lgsdir2lem2  15745  lgsdir2lem4  15747  lgsdir2lem5  15748  lgsdi  15753  gausslemma2dlem0i  15773  gausslemma2dlem4  15780  lgseisenlem4  15789  lgsquadlem1  15793  lgsquad2lem2  15798  lgsquad2  15799  m1lgs  15801  2lgs2  15818  2lgslem4  15819  2lgsoddprmlem2  15822  2lgsoddprmlem3c  15825  2lgsoddprmlem3d  15826  2sqlem9  15840  2sqlem10  15841  1vgrex  15858  vtxval0  15891  iedgval0  15892  uhgr0  15922  upgrfi  15939  umgrislfupgrdom  15966  ausgrusgrben  16003  uspgredgiedg  16013  uspgriedgedg  16014  usgrislfuspgrdom  16025  uspgredg2vlem  16055  uspgredg2v  16056  usgr0  16074  griedg0prc  16085  0wlk0  16159  clwwlkn1  16203  clwwlkn2  16206  ex-fl  16231  ex-ceil  16232  ex-exp  16233  ex-fac  16234  ex-gcd  16237  bj-stfal  16248  bj-stst  16251  bj-dcfal  16261  bj-dcdc  16265  bj-stdc  16266  bj-dcst  16267  bj-el2oss1o  16280  elabf2  16288  bd0  16329  bdeli  16351  bdcriota  16388  bdbm1.3ii  16396  bdinex1  16404  bdssexi  16408  bj-inex  16412  bj-snex  16418  bj-sucex  16428  bj-d0clsepcl  16430  bj-omind  16439  bj-om  16442  bj-2inf  16443  bj-peano2  16444  bdpeano5  16448  bj-omssonALT  16468  bj-inf2vnlem1  16475  bj-omex2  16482  bj-nn0sucALT  16483  3dom  16497  012of  16502  2o01f  16503  subctctexmid  16511  pw1dceq  16515  nninfall  16521  nninfsellemqall  16527  nninfsellemeqinf  16528  nninfomnilem  16530  nninfomni  16531  exmidsbthrlem  16536  sbthom  16540  isomninnlem  16544  isomninn  16545  cvgcmp2nlemabs  16546  iooreen  16549  trilpolemisumle  16552  trilpolemeq1  16554  trilpo  16557  trirec0  16558  apdifflemr  16561  iswomninnlem  16563  iswomninn  16564  ismkvnnlem  16566  ismkvnn  16567  redcwlpo  16569  dcapnconst  16575  nconstwlpolem0  16577  nconstwlpo  16580  neapmkv  16582  neap0mkv  16583  taupi  16587