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 𝜑 is true, and 𝜑 implies 𝜓, then 𝜓 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	⊢ 𝜑
maj	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ax-mp	⊢ 𝜓

Detailed syntax breakdown of Axiom ax-mp

Step	Hyp	Ref	Expression
1		wps	1 wff 𝜓

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  2790  elv  2803  elexi  2812  ceqsal  2829  vtocl3  2857  vtoclef  2876  vtocle  2877  spcv  2897  spcev  2898  clel3  2938  elabf  2946  elab2  2951  elab3  2955  euxfrdc  2989  reueq  3002  rmoimi2  3006  sbsbc  3032  sbc8g  3036  sbc6  3054  sbcie  3063  sbcrex  3108  csbvarg  3152  csbief  3169  csbie2  3174  sbnfc2  3185  sseli  3220  sselii  3221  sseq1i  3250  sseq2i  3251  difeq1i  3318  difeq2i  3319  uneq1i  3354  uneq2i  3355  ineq1i  3401  ineq2i  3402  ssinss1  3433  difdif2ss  3461  n0ii  3500  ne0ii  3501  vn0  3502  vn0m  3503  abf  3535  disj2  3547  difid  3560  0dif  3563  disjdif  3564  difin0  3565  undif1ss  3566  difdifdirss  3576  iftruei  3608  iffalsei  3611  ifbieq2i  3626  ifbieq12i  3628  pweqi  3653  pwid  3664  sneqi  3678  elsn  3682  elpr  3687  elsn2  3700  ralsn  3709  rexsn  3710  eltp  3714  rabrsndc  3734  preq1i  3746  preq2i  3747  prid1  3772  snnz  3786  snm  3787  prnz  3790  prm  3791  tpnz  3793  snss  3803  snsssn  3839  opeq1i  3860  opeq2i  3861  unieqi  3898  unissi  3911  inteqi  3927  intmin2  3949  intab  3952  intsn  3958  iinconstm  3974  iuniin  3975  iinss1  3977  iunxdif2  4014  ssiinf  4015  iinss  4017  iinss2  4018  iinab  4027  iundif2ss  4031  iindif2m  4033  iinin2m  4034  iunxsn  4042  iunxprg  4046  iinpw  4056  invdisjrab  4077  sndisj  4079  disjxsn  4081  breqi  4089  breq1i  4090  breq2i  4091  brab1  4131  opabbii  4151  truni  4196  bm1.3ii  4205  a9evsep  4206  ax9vsep  4207  zfnuleu  4208  axnul  4209  ssexi  4222  rabex  4228  rabex2  4230  elpw2  4241  pwnss  4243  iin0r  4253  intv  4254  pwex  4267  snex  4269  notnotsnex  4271  ord3ex  4274  dtruarb  4275  undifexmid  4277  intid  4310  opnzi  4321  copsexg  4330  opwo0id  4335  opelopabf  4363  epelc  4382  elon  4465  inton  4484  onn0  4491  onm  4492  elsuc  4497  elsuc2  4498  sucid  4508  iunsuc  4511  onordi  4517  ontrci  4518  onelssi  4520  eusvnf  4544  ssonunii  4581  sucex  4591  onssi  4607  onsuci  4608  ordtriexmidlem  4611  ordtriexmidlem2  4612  ordtriexmid  4613  ontriexmidim  4614  ordtri2orexmid  4615  2ordpr  4616  ontr2exmid  4617  onsucsssucexmid  4619  onsucelsucexmid  4622  regexmidlemm  4624  reg2exmid  4628  onirri  4635  ruALT  4643  onprc  4644  sucon  4645  dtru  4652  0elsucexmid  4657  ordpwsucexmid  4662  ordtri2or2exmid  4663  ontri2orexmidim  4664  dcextest  4673  omex  4685  find  4691  omelon  4701  nnoni  4703  limom  4706  nnregexmid  4713  omsinds  4714  xpeq1i  4739  xpeq2i  4740  0nelxp  4747  opthprc  4770  mosubop  4785  releqi  4802  relssi  4810  relin1  4837  relin2  4838  reldif  4839  inopab  4854  difopab  4855  xpiindim  4859  opabbi2dv  4871  ideq  4874  coeq1i  4881  coeq2i  4882  cnveqi  4897  eldm  4920  eldm2  4921  dmeqi  4924  dmv  4939  rneqi  4952  elrnmpti  4977  dmex  4991  rnex  4992  reseq1i  5001  reseq2i  5002  residm  5037  resex  5046  resmpt3  5054  imaeq1i  5065  imaeq2i  5066  elima  5073  imaex  5083  elimasn  5095  args  5097  epini  5099  dfse2  5101  eliniseg2  5108  relbrcnv  5109  cotr  5110  issref  5111  cnvsym  5112  asymref  5114  intirr  5115  codir  5117  qfto  5118  ssrnres  5171  cnveq0  5185  cnvsn0  5197  dmsnop  5202  rnsnop  5209  resdm2  5219  dfco2a  5229  cocnvcnv1  5239  coi2  5245  coires1  5246  cnvssrndm  5250  cossxp  5251  cocnvres  5253  relrelss  5255  relcoi2  5259  unidmrn  5261  dfdm2  5263  unixpm  5264  cnvexg  5266  cnvex  5267  cnviinm  5270  iotaval  5290  funeqi  5339  funi  5350  funres  5359  funcnvsn  5366  funcnvcnv  5380  funin  5392  funcnvres  5394  isarep2  5408  fneq1i  5415  fneq2i  5416  fndmi  5421  fnresdisj  5433  fnresi  5441  mpt0  5451  dmmpti  5453  feq1i  5466  feq2i  5467  fdmi  5481  fun2  5498  fssres  5501  resasplitss  5505  fintm  5511  fconst6  5525  f1ores  5587  foimacnv  5590  resdif  5594  funcocnv2  5597  f10d  5607  f1ovi  5612  fveq1i  5628  fveq2i  5630  0fv  5665  fvun1  5700  fvopab3ig  5708  fvmptss2  5709  mptrcl  5717  elfvmptrab1  5729  fndmdif  5740  fneqeql2  5744  f1oresrab  5800  fmptco  5801  funopsn  5817  fnressn  5825  fressnfv  5826  fmptap  5829  fvsnun1  5836  fvsnun2  5837  fsnunfv  5840  fconst2  5856  mptex  5865  riotabiia  5973  acexmidlema  5992  acexmidlemb  5993  acexmidlemcase  5996  acexmidlem2  5998  acexmidlemv  5999  oveq1i  6011  oveq2i  6012  oveqi  6014  oprabidlem  6032  0neqopab  6049  oprabbii  6059  oprabss  6090  mpompt  6096  funoprab  6104  fnoprab  6107  ovigg  6125  elmpocl  6200  relmptopab  6207  resfunexgALT  6253  cofunexg  6254  mptexw  6258  opabex3d  6266  opabex3  6267  1st0  6290  2nd0  6291  op1st  6292  op2nd  6293  f1stres  6305  f2ndres  6306  fo1stresm  6307  fo2ndresm  6308  1stcof  6309  2ndcof  6310  1stexg  6313  2ndexg  6314  releldm2  6331  reldm  6332  dfoprab3  6337  mpomptsx  6343  mpompts  6344  fnmpoi  6349  dmmpo  6350  mpoexxg  6356  mpoexw  6359  1stconst  6367  2ndconst  6368  dfmpo  6369  algrflem  6375  algrflemg  6376  cnvoprab  6380  f1od2  6381  mpoxopn0yelv  6385  mpoxopoveq  6386  tposssxp  6395  brtpos2  6397  reldmtpos  6399  dftpos2  6407  dftpos4  6409  tpostpos  6410  tpostpos2  6411  tposfo  6417  tposf  6418  tposeqi  6423  tposex  6424  tposoprab  6426  issmo  6434  smores  6438  smores2  6440  iordsmo  6443  smo0  6444  tfrlem8  6464  tfrexlem  6480  tfr1onlem3  6484  tfr1onlemsucaccv  6487  tfr1onlembxssdm  6489  tfr1onlemres  6495  tfri1dALT  6497  tfri2  6512  rdgisuc1  6530  rdg0  6533  frecfun  6541  frec0g  6543  freccllem  6548  frecfcllem  6550  frecsuclem  6552  frecrdg  6554  2on0  6572  xp01disj  6579  2oconcl  6585  fnoa  6593  oaexg  6594  fnom  6596  omexg  6597  fnoei  6598  oeiexg  6599  oei0  6605  oacl  6606  oasuc  6610  o1p1e2  6614  omsuc  6618  nna0r  6624  nnm0r  6625  1onn  6666  2onn  6667  3onn  6668  4onn  6669  2ssom  6670  eqerlem  6711  eceq2i  6718  elqs  6733  qsex  6739  ecqs  6744  iinerm  6754  th3qlem1  6784  th3q  6787  mapsn  6837  mapsnf1o3  6844  ixpiinm  6871  ixpssmap  6879  brdom  6899  f1dom  6911  enref  6916  dom2  6926  idssen  6928  ssdomg  6930  ensymi  6934  ensn1  6948  fiprc  6968  1domsn  6976  dom1o  6977  xpcomf1o  6984  xpcomco  6985  dom0  6999  0dom  7000  xpmapenlem  7010  phplem2  7014  php5  7019  snnen2og  7020  1nen2  7022  php5dom  7024  ssfilem  7037  ssfiexmid  7038  domfiexmid  7040  0fin  7046  diffitest  7049  findcard  7050  findcard2  7051  findcard2s  7052  isinfinf  7059  ac6sfi  7060  inffiexmid  7068  pw1fin  7072  unfiexmid  7080  xpfi  7094  fisseneq  7096  ssfirab  7098  residfi  7107  en1eqsn  7115  snexxph  7117  sbthlem2  7125  sbthlemi3  7126  sbthlemi6  7129  sbthlem7  7130  fi0  7142  supeq1i  7155  infeq1i  7180  djuexb  7211  djuf1olemr  7221  inresflem  7227  djuinr  7230  updjudhcoinlf  7247  updjudhcoinrg  7248  casefun  7252  caserel  7254  caseinj  7256  caseinl  7258  caseinr  7259  omp1eomlem  7261  endjusym  7263  difinfsn  7267  difinfinf  7268  djuinj  7273  0ct  7274  ctmlemr  7275  ctssdclemn0  7277  ctssdccl  7278  omct  7284  ctfoex  7285  finomni  7307  exmidomni  7309  fodjuomni  7316  ctssexmid  7317  fodjumkv  7327  nninfwlporlem  7340  nninfwlpoimlemg  7342  nninfwlpoim  7346  nninfinfwlpo  7347  card0  7360  ficardon  7361  exmidonfinlem  7371  dju1p1e2  7375  exmidfodomrlemim  7379  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  iftrueb01  7408  3nelsucpw1  7419  sucpw1nss3  7420  3nsssucpw1  7421  2onetap  7441  exmidmotap  7447  0npi  7500  dmaddpi  7512  dmmulpi  7513  1lt2pi  7527  0nnq  7551  1nq  7553  dmaddpq  7566  dmmulpq  7567  rec1nq  7582  1lt2nq  7593  halfnqq  7597  prarloclemarch2  7606  enq0enq  7618  nqnq0pi  7625  nnnq0lem1  7633  addnnnq0  7636  mulnnnq0  7637  nq0m0r  7643  addpinq1  7651  prarloclem5  7687  prarloclemcalc  7689  1pr  7741  1idprl  7777  1idpru  7778  ltexprlemm  7787  recexprlem1ssl  7820  recexprlem1ssu  7821  suplocexprlemell  7900  suplocexprlem2b  7901  suplocexprlemmu  7905  suplocexprlemdisj  7907  suplocexprlemloc  7908  suplocexprlemub  7910  suplocexprlemlub  7911  prsrlem1  7929  addsrpr  7932  mulsrpr  7933  gt0srpr  7935  0nsr  7936  0r  7937  1sr  7938  m1r  7939  m1m1sr  7948  caucvgsr  7989  suplocsrlempr  7994  addresr  8024  mulresr  8025  pitonnlem1  8032  peano1nnnn  8039  axi2m1  8062  axcnre  8068  peano5nnnn  8079  axcaucvg  8087  mpomulf  8136  mulridi  8148  mullidi  8149  pnfnre  8188  mnfnre  8189  pnfnemnf  8201  mnfxr  8203  rexri  8204  ltnri  8239  ltleii  8249  00id  8287  addridi  8288  addlidi  8289  0cnALT  8336  negeqi  8340  negicn  8347  neg0  8392  renegcli  8408  negcli  8414  negidi  8415  negnegi  8416  subidi  8417  subid1i  8418  negne0bi  8419  negrebi  8420  mul02i  8536  mul01i  8537  mulm1i  8549  leidi  8632  gt0ne0ii  8634  inelr  8731  msqge0i  8764  gt0ap0ii  8775  1div1e1  8851  div1i  8887  eqnegi  8888  recclapi  8889  recidapi  8890  divmulapi  8913  rerecclapi  8924  redivclapi  8926  rerecapb  8990  recgt0  8997  ltp1i  9052  divgt0ii  9066  ltmul1ii  9075  ltdiv1ii  9076  sup3exmid  9104  peano5nni  9113  nnrei  9119  1nn  9121  nngt0i  9140  neg1ap0  9219  2timesi  9240  times2i  9241  2nn  9272  3nn  9273  4nn  9274  5nn  9275  6nn  9276  7nn  9277  8nn  9278  9nn  9279  2muline0  9336  rehalfcli  9360  nn0ssre  9373  nnnn0i  9377  dfn2  9382  0nn0  9384  nn0ge0i  9396  zrei  9452  neg1z  9478  nn0negzi  9481  dfz2  9519  nneoi  9551  peano5uzi  9556  dfuzi  9557  nn0ind-raph  9564  deceq1i  9584  deceq2i  9585  10nn  9593  numltc  9603  eluzel2  9727  eluz1i  9729  nn0uz  9757  nnuz  9758  infrenegsupex  9789  lbzbi  9811  divfnzn  9816  qdivcl  9838  irrmul  9842  irrmulap  9843  cnref1o  9846  0ltpnf  9978  mnflt0  9980  0lepnf  9986  xrltnsym  9989  xrlttri3  9993  nltpnft  10010  ngtmnft  10013  xrrebnd  10015  xnegmnf  10025  xneg0  10027  xltnegi  10031  xaddmnf1  10044  xaddmnf2  10045  mnfaddpnf  10047  xaddid1  10058  xnn0lenn0nn0  10061  xnn0xadd0  10063  xposdif  10078  ixxex  10095  iooval2  10111  unirnioo  10169  ioorebasg  10171  elrege0  10172  fzval2  10207  fzen  10239  fzprval  10278  fztpval  10279  uzdisj  10289  ige2m1fz  10306  fz01or  10307  fz1ssfz0  10313  fz0sn  10317  fz0tp  10318  fz0to3un2pr  10319  fz0to4untppr  10320  nn0disj  10334  1fv  10335  4fvwrd4  10336  fzo0ss1  10372  fzo01  10422  fzo12sn  10423  fzo0to2pr  10424  fzo0to3tp  10425  fzo0to42pr  10426  zsupssdc  10458  qbtwnxr  10477  flval  10492  fldiv4lem1div2  10527  modqfrac  10559  modqmulnn  10564  q2txmodxeq0  10606  frecuzrdgdom  10640  frecuzrdgfun  10642  frecuzrdgsuct  10646  frechashgf1o  10650  nnct  10657  xnn0nnen  10659  fxnn0nninf  10661  0tonninf  10662  1tonninf  10663  iseqvalcbv  10681  ser0f  10756  0exp0e1  10766  qexpcl  10777  qexpclz  10782  m1expcl2  10783  1exp  10790  sqvali  10841  sqcli  10842  sqeq0i  10843  resqcli  10846  sq1  10855  neg1sqe1  10856  iexpcyc  10866  qsqeqor  10872  facnn  10949  fac0  10950  fac1  10951  fac2  10953  fac3  10954  fac4  10955  bcval  10971  bcm1k  10982  bcpasc  10988  bccl  10989  4bc3eq4  10995  4bc2eq6  10996  hashinfom  11000  hashennn  11002  hashfz1  11005  fihasheq0  11015  hash0  11018  hashsng  11020  fihashen1  11021  omgadd  11024  hashp1i  11032  hashxp  11048  fimaxq  11049  zfz1iso  11063  hash2en  11065  wrdexi  11084  wrdv  11087  wrdeqi  11094  wrd0  11096  lsw0  11119  ccatclab  11129  ccatidid  11145  s1prc  11156  ccat1st1st  11172  swrds1  11200  fnpfx  11209  swrdccatin2  11261  pfxccatin12lem2  11263  cats1fvn  11296  shftidt2  11343  cjexp  11404  re0  11406  im0  11407  re1  11408  im1  11409  cj0  11412  cji  11413  recli  11422  imcli  11423  cjcli  11424  replimi  11425  cjcji  11426  reim0bi  11427  rerebi  11428  cjrebi  11429  recji  11430  imcji  11431  cjmulrcli  11432  cjmulvali  11433  cjmulge0i  11434  renegi  11435  imnegi  11436  cjnegi  11437  addcji  11438  uzin2  11498  rexanuz  11499  rexfiuz  11500  sqrtrval  11511  sqrt0  11515  resqrexlemcalc3  11527  resqrexlemcvg  11530  resqrex  11537  abs0  11569  absi  11570  qabsor  11586  absimle  11595  recan  11620  caubnd2  11628  leabsi  11639  absrei  11640  sqrtpclii  11641  sqrtgt0ii  11642  absvalsqi  11651  absvalsq2i  11652  abscli  11653  absge0i  11654  absval2i  11655  abs00i  11656  absgt0api  11657  absnegi  11658  abscji  11659  releabsi  11660  infxrnegsupex  11774  xrbdtri  11787  cbvsum  11871  sumeq1i  11874  sum0  11899  isumz  11900  fisumss  11903  fsumsersdc  11906  fsumadd  11917  isumclim  11932  isumclim3  11934  fsumcnv  11948  modfsummodlem1  11967  fsumrelem  11982  binomlem  11994  binom  11995  arisum2  12010  expcnv  12015  0.999...  12032  prodf1f  12054  cbvprod  12069  prodeq1i  12072  zproddc  12090  zprodap0  12092  prod0  12096  fprodssdc  12101  prodsnf  12103  fprodcnv  12136  fprodge0  12148  fprodge1  12150  ef0lem  12171  esum  12173  ere  12181  ege2le3  12182  ef0  12183  eff2  12191  efsep  12202  reeff1  12211  sin0  12240  cos0  12241  ef01bndlem  12267  cos2bnd  12271  sincos1sgn  12276  sincos2sgn  12277  sin4lt0  12278  eirr  12290  0dvds  12322  dvds1  12364  z0even  12422  n2dvdsm1  12424  z2even  12425  n2dvds3  12426  ndvdssub  12441  ndvdsi  12444  flodddiv4  12447  bits0  12459  bitsfzo  12466  0bits  12470  m1bits  12471  bitsinv1lem  12472  bitsinv1  12473  gcddvds  12484  gcd1  12508  6gcd4e2  12516  bezoutlembi  12526  dfgcd3  12531  dfgcd2  12535  nninfctlemfo  12561  nninfct  12562  3lcm2e6woprm  12608  qredeu  12619  isprm2lem  12638  isprm3  12640  prm2orodd  12648  isprm5lem  12663  sqrt2irr0  12686  pw2dvds  12688  phicl2  12736  phi1  12741  dfphi2  12742  phiprmpw  12744  eulerthlemrprm  12751  eulerthlemh  12753  odzval  12764  oddprm  12782  pczpre  12820  pcdiv  12825  pc0  12827  pcqdiv  12830  pcrec  12831  pcexp  12832  pcxcl  12834  pcxqcl  12835  pcdvdstr  12850  pc2dvds  12853  dvdsprmpweqnn  12859  pcmpt  12866  qexpz  12875  pockthi  12881  1arith2  12891  4sqlemffi  12919  4sqlem11  12924  4sqlem13m  12926  4sqlem19  12932  dec2dvds  12934  dec5nprm  12937  modxai  12939  modxp1i  12941  numexp0  12945  numexp1  12946  ennnfonelemp1  12977  ennnfonelem1  12978  ennnfonelemkh  12983  ennnfonelemex  12985  ennnfonelemnn0  12993  ennnfonelemr  12994  exmidunben  12997  ctinfomlemom  12998  ctinfom  12999  ctinf  13001  qnnen  13002  omctfn  13014  omiunct  13015  ssnnctlemct  13017  nninfdc  13024  structcnvcnv  13048  structfun  13050  structfn  13051  ndxarg  13055  ndxid  13056  setsresg  13070  setsslnid  13084  basmex  13092  basmexd  13093  strleun  13137  strle1g  13139  prdsex  13302  prdsvallem  13305  prdsval  13306  prdsbaslemss  13307  imasaddfnlemg  13347  quslem  13357  xpsfrnel  13377  xpsff1o  13382  ismgmn0  13391  fn0g  13408  0g0  13409  fngsum  13421  idghm  13796  rhmfn  14136  rmodislmodlem  14314  rmodislmod  14315  lidlmex  14439  mopnset  14516  cntopex  14518  cnfldex  14523  cnfldbas  14524  mpocnfldadd  14525  mpocnfldmul  14527  cnfldcj  14529  cnfldtset  14530  cnfldle  14531  cnfldds  14532  cnring  14534  cnfld0  14535  cnfld1  14536  cnfldneg  14537  cnfldplusf  14538  cnfldsub  14539  cnfldmulg  14540  cnfldexp  14541  cnsubglem  14543  cnsubrglem  14544  gzsubrg  14546  gsumfzfsumlem0  14550  cnfldui  14553  zringring  14557  zringabl  14558  zringgrp  14559  zring1  14565  zringsubgval  14569  expghmap  14571  znval  14600  znle  14601  znbaslemnn  14603  znbas  14608  znzrh2  14610  znzrhval  14611  znzrhfo  14612  znleval  14617  znidom  14621  znidomb  14622  fnpsr  14631  psrelbas  14639  psradd  14643  psraddcl  14644  psr1clfi  14652  mplrcl  14658  mplbasss  14660  mpladd  14668  istopon  14687  topontopi  14690  toponunii  14691  toponrestid  14695  istps  14706  topontopn  14711  eltpsi  14715  eltg4i  14729  eltg3  14731  tg1  14733  tg2  14734  tgclb  14739  topnex  14760  sn0topon  14762  distps  14765  cldrcl  14776  sn0cld  14811  restco  14848  lmrcl  14866  ssidcn  14884  cnconst2  14907  cnptopresti  14912  cnptoprest  14913  txuni2  14930  txbas  14932  eltx  14933  txcnp  14945  upxp  14946  txcnmpt  14947  uptx  14948  txcn  14949  txrest  14950  txlm  14953  cnmptid  14955  cnmpt1st  14962  cnmpt2nd  14963  hmeofn  14976  psmetge0  15005  ismeti  15020  xmetunirn  15032  xmetge0  15039  unirnblps  15096  unirnbl  15097  mopnex  15179  qtopbasss  15195  retop  15198  uniretop  15199  iooretopg  15202  cnxmet  15205  cntoptopon  15206  cnbl0  15208  cnfldxms  15211  cnfldtps  15212  rexmet  15223  blssioo  15227  tgioo  15228  tgqioo  15229  cnopnap  15285  hovercncf  15320  limcresi  15340  dvfvalap  15355  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvcnp2cntop  15373  dvcoapbr  15381  dvexp2  15386  dvrecap  15387  dveflem  15400  dvef  15401  plyun0  15410  plyrecj  15437  dvply2  15441  reeff1o  15447  sin0pilem1  15455  sin0pilem2  15456  pilem3  15457  pigt2lt4  15458  pire  15460  sinhalfpilem  15465  pidiv2halves  15469  cosneghalfpi  15472  cospi  15474  efipi  15475  sin2pi  15477  cos2pi  15478  ef2pi  15479  cosq14gt0  15506  coseq00topi  15509  coseq0negpitopi  15510  sincos4thpi  15514  sincos6thpi  15516  sincos3rdpi  15517  pigt3  15518  cos02pilt1  15525  ioocosf1o  15528  dfrelog  15534  relogf1o  15535  relogcl  15536  relogiso  15547  rpcxpsqrt  15596  rpabscxpbnd  15614  2logb9irr  15645  2logb9irrALT  15648  sqrt2cxp2logb9e3  15649  2irrexpq  15650  2logb9irrap  15651  2irrexpqap  15652  mpodvdsmulf1o  15664  fsumdvdsmul  15665  perfectlem2  15674  lgsdir2lem1  15707  lgsdir2lem2  15708  lgsdir2lem4  15710  lgsdir2lem5  15711  lgsdi  15716  gausslemma2dlem0i  15736  gausslemma2dlem4  15743  lgseisenlem4  15752  lgsquadlem1  15756  lgsquad2lem2  15761  lgsquad2  15762  m1lgs  15764  2lgs2  15781  2lgslem4  15782  2lgsoddprmlem2  15785  2lgsoddprmlem3c  15788  2lgsoddprmlem3d  15789  2sqlem9  15803  2sqlem10  15804  1vgrex  15821  vtxval0  15854  iedgval0  15855  uhgr0  15885  upgrfi  15902  umgrislfupgrdom  15929  ausgrusgrben  15966  uspgredgiedg  15976  uspgriedgedg  15977  usgrislfuspgrdom  15988  uspgredg2vlem  16018  uspgredg2v  16019  0wlk0  16082  ex-fl  16089  ex-ceil  16090  ex-exp  16091  ex-fac  16092  ex-gcd  16095  bj-stfal  16106  bj-stst  16109  bj-dcfal  16119  bj-dcdc  16123  bj-stdc  16124  bj-dcst  16125  bj-el2oss1o  16138  elabf2  16146  bd0  16187  bdeli  16209  bdcriota  16246  bdbm1.3ii  16254  bdinex1  16262  bdssexi  16266  bj-inex  16270  bj-snex  16276  bj-sucex  16286  bj-d0clsepcl  16288  bj-omind  16297  bj-om  16300  bj-2inf  16301  bj-peano2  16302  bdpeano5  16306  bj-omssonALT  16326  bj-inf2vnlem1  16333  bj-omex2  16340  bj-nn0sucALT  16341  012of  16357  2o01f  16358  subctctexmid  16366  nninfall  16375  nninfsellemqall  16381  nninfsellemeqinf  16382  nninfomnilem  16384  nninfomni  16385  exmidsbthrlem  16390  sbthom  16394  isomninnlem  16398  isomninn  16399  cvgcmp2nlemabs  16400  iooreen  16403  trilpolemisumle  16406  trilpolemeq1  16408  trilpo  16411  trirec0  16412  apdifflemr  16415  iswomninnlem  16417  iswomninn  16418  ismkvnnlem  16420  ismkvnn  16421  redcwlpo  16423  dcapnconst  16429  nconstwlpolem0  16431  nconstwlpo  16434  neapmkv  16436  neap0mkv  16437  taupi  16441