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 664.

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  640  notnoti  646  pm2.21i  647  pm2.24ii  648  notbii  670  nbn  701  ori  725  orci  733  olci  734  biorfi  748  imorri  751  dcbii  842  simp1i  1009  simp2i  1010  simp3i  1011  3mix1i  1172  3mix2i  1173  3mix3i  1174  3jaoi  1316  mptru  1382  dfnot  1391  mptnan  1443  mtpor  1445  mtpxor  1446  dcfromnotnotr  1468  dcfromcon  1469  dcfrompeirce  1470  mpg  1475  19.23h  1522  hbequid  1537  axi12  1538  nfri  1543  spi  1560  19.21  1607  eximii  1626  19.35i  1649  nfn  1682  19.37aiv  1699  19.23  1702  exan  1717  equid  1725  hbae  1742  equvini  1782  equveli  1783  sbid  1798  sbieh  1814  exdistrfor  1824  dveeq2or  1840  ax11v  1851  ax11ev  1852  equs5or  1854  sb4or  1857  sb4bor  1859  nfsb2or  1861  sbequilem  1862  sbequi  1863  speiv  1886  nfsbxy  1971  nfsbxyt  1972  sbco  1997  sbcocom  1999  sbcomxyyz  2001  sbal1yz  2030  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  eumoi  2088  moani  2125  elsb1  2184  elsb2  2185  eqeq1i  2214  eqeq2i  2217  eleq1i  2272  eleq2i  2273  nfcrii  2342  neeq1i  2392  neeq2i  2393  necon3i  2425  rspec  2559  rgen2a  2561  mprg  2564  r19.21  2583  r19.23  2615  raleqi  2707  rexeqi  2708  rabeqif  2764  elv  2777  elexi  2785  ceqsal  2802  vtocl3  2830  vtoclef  2847  vtocle  2848  spcv  2868  spcev  2869  clel3  2909  elabf  2917  elab2  2922  elab3  2926  euxfrdc  2960  reueq  2973  rmoimi2  2977  sbsbc  3003  sbc8g  3007  sbc6  3025  sbcie  3034  sbcrex  3079  csbvarg  3122  csbief  3139  csbie2  3144  sbnfc2  3155  sseli  3190  sselii  3191  sseq1i  3220  sseq2i  3221  difeq1i  3288  difeq2i  3289  uneq1i  3324  uneq2i  3325  ineq1i  3371  ineq2i  3372  ssinss1  3403  difdif2ss  3431  n0ii  3470  ne0ii  3471  vn0  3472  vn0m  3473  abf  3505  disj2  3517  difid  3530  0dif  3533  disjdif  3534  difin0  3535  undif1ss  3536  difdifdirss  3546  iftruei  3578  iffalsei  3581  ifbieq2i  3595  ifbieq12i  3597  pweqi  3621  pwid  3632  sneqi  3646  elsn  3650  elpr  3655  elsn2  3668  ralsn  3677  rexsn  3678  eltp  3682  rabrsndc  3702  preq1i  3714  preq2i  3715  prid1  3740  snnz  3753  snm  3754  prnz  3757  prm  3758  tpnz  3760  snss  3770  snsssn  3804  opeq1i  3824  opeq2i  3825  unieqi  3862  unissi  3875  inteqi  3891  intmin2  3913  intab  3916  intsn  3922  iinconstm  3938  iuniin  3939  iinss1  3941  iunxdif2  3978  ssiinf  3979  iinss  3981  iinss2  3982  iinab  3991  iundif2ss  3995  iindif2m  3997  iinin2m  3998  iunxsn  4006  iunxprg  4010  iinpw  4020  invdisjrab  4041  sndisj  4043  disjxsn  4045  breqi  4053  breq1i  4054  breq2i  4055  brab1  4095  opabbii  4115  truni  4160  bm1.3ii  4169  a9evsep  4170  ax9vsep  4171  zfnuleu  4172  axnul  4173  ssexi  4186  rabex  4192  rabex2  4194  elpw2  4205  pwnss  4207  iin0r  4217  intv  4218  pwex  4231  snex  4233  notnotsnex  4235  ord3ex  4238  dtruarb  4239  undifexmid  4241  intid  4272  opnzi  4283  copsexg  4292  opwo0id  4297  opelopabf  4325  epelc  4342  elon  4425  inton  4444  onn0  4451  onm  4452  elsuc  4457  elsuc2  4458  sucid  4468  iunsuc  4471  onordi  4477  ontrci  4478  onelssi  4480  eusvnf  4504  ssonunii  4541  sucex  4551  onssi  4567  onsuci  4568  ordtriexmidlem  4571  ordtriexmidlem2  4572  ordtriexmid  4573  ontriexmidim  4574  ordtri2orexmid  4575  2ordpr  4576  ontr2exmid  4577  onsucsssucexmid  4579  onsucelsucexmid  4582  regexmidlemm  4584  reg2exmid  4588  onirri  4595  ruALT  4603  onprc  4604  sucon  4605  dtru  4612  0elsucexmid  4617  ordpwsucexmid  4622  ordtri2or2exmid  4623  ontri2orexmidim  4624  dcextest  4633  omex  4645  find  4651  omelon  4661  nnoni  4663  limom  4666  nnregexmid  4673  omsinds  4674  xpeq1i  4699  xpeq2i  4700  0nelxp  4707  opthprc  4730  mosubop  4745  releqi  4762  relssi  4770  relin1  4797  relin2  4798  reldif  4799  inopab  4814  difopab  4815  xpiindim  4819  opabbi2dv  4831  ideq  4834  coeq1i  4841  coeq2i  4842  cnveqi  4857  eldm  4880  eldm2  4881  dmeqi  4884  dmv  4899  rneqi  4911  elrnmpti  4936  dmex  4950  rnex  4951  reseq1i  4960  reseq2i  4961  residm  4996  resex  5005  resmpt3  5013  imaeq1i  5024  imaeq2i  5025  elima  5032  imaex  5042  elimasn  5054  args  5056  epini  5058  dfse2  5060  eliniseg2  5067  relbrcnv  5068  cotr  5069  issref  5070  cnvsym  5071  asymref  5073  intirr  5074  codir  5076  qfto  5077  ssrnres  5130  cnveq0  5144  cnvsn0  5156  dmsnop  5161  rnsnop  5168  resdm2  5178  dfco2a  5188  cocnvcnv1  5198  coi2  5204  coires1  5205  cnvssrndm  5209  cossxp  5210  cocnvres  5212  relrelss  5214  relcoi2  5218  unidmrn  5220  dfdm2  5222  unixpm  5223  cnvexg  5225  cnvex  5226  cnviinm  5229  iotaval  5248  funeqi  5297  funi  5308  funres  5317  funcnvsn  5324  funcnvcnv  5338  funin  5350  funcnvres  5352  isarep2  5366  fneq1i  5373  fneq2i  5374  fndmi  5379  fnresdisj  5391  fnresi  5399  mpt0  5409  dmmpti  5411  feq1i  5424  feq2i  5425  fdmi  5439  fun2  5455  fssres  5458  resasplitss  5462  fintm  5468  fconst6  5482  f1ores  5544  foimacnv  5547  resdif  5551  funcocnv2  5554  f1ovi  5568  fveq1i  5584  fveq2i  5586  0fv  5619  fvun1  5652  fvopab3ig  5660  fvmptss2  5661  mptrcl  5669  elfvmptrab1  5681  fndmdif  5692  fneqeql2  5696  f1oresrab  5752  fmptco  5753  funopsn  5769  fnressn  5777  fressnfv  5778  fmptap  5781  fvsnun1  5788  fvsnun2  5789  fsnunfv  5792  fconst2  5808  mptex  5817  riotabiia  5924  acexmidlema  5942  acexmidlemb  5943  acexmidlemcase  5946  acexmidlem2  5948  acexmidlemv  5949  oveq1i  5961  oveq2i  5962  oveqi  5964  oprabidlem  5982  0neqopab  5997  oprabbii  6007  oprabss  6038  mpompt  6044  funoprab  6052  fnoprab  6055  ovigg  6073  elmpocl  6148  resfunexgALT  6200  cofunexg  6201  mptexw  6205  opabex3d  6213  opabex3  6214  1st0  6237  2nd0  6238  op1st  6239  op2nd  6240  f1stres  6252  f2ndres  6253  fo1stresm  6254  fo2ndresm  6255  1stcof  6256  2ndcof  6257  1stexg  6260  2ndexg  6261  releldm2  6278  reldm  6279  dfoprab3  6284  mpomptsx  6290  mpompts  6291  fnmpoi  6296  dmmpo  6297  mpoexxg  6303  mpoexw  6306  1stconst  6314  2ndconst  6315  dfmpo  6316  algrflem  6322  algrflemg  6323  cnvoprab  6327  f1od2  6328  mpoxopn0yelv  6332  mpoxopoveq  6333  tposssxp  6342  brtpos2  6344  reldmtpos  6346  dftpos2  6354  dftpos4  6356  tpostpos  6357  tpostpos2  6358  tposfo  6364  tposf  6365  tposeqi  6370  tposex  6371  tposoprab  6373  issmo  6381  smores  6385  smores2  6387  iordsmo  6390  smo0  6391  tfrlem8  6411  tfrexlem  6427  tfr1onlem3  6431  tfr1onlemsucaccv  6434  tfr1onlembxssdm  6436  tfr1onlemres  6442  tfri1dALT  6444  tfri2  6459  rdgisuc1  6477  rdg0  6480  frecfun  6488  frec0g  6490  freccllem  6495  frecfcllem  6497  frecsuclem  6499  frecrdg  6501  2on0  6519  xp01disj  6526  2oconcl  6532  fnoa  6540  oaexg  6541  fnom  6543  omexg  6544  fnoei  6545  oeiexg  6546  oei0  6552  oacl  6553  oasuc  6557  o1p1e2  6561  omsuc  6565  nna0r  6571  nnm0r  6572  1onn  6613  2onn  6614  3onn  6615  4onn  6616  2ssom  6617  eqerlem  6658  eceq2i  6665  elqs  6680  qsex  6686  ecqs  6691  iinerm  6701  th3qlem1  6731  th3q  6734  mapsn  6784  mapsnf1o3  6791  ixpiinm  6818  ixpssmap  6826  brdom  6846  f1dom  6858  enref  6863  dom2  6873  idssen  6875  ssdomg  6877  ensymi  6881  ensn1  6895  fiprc  6914  1domsn  6921  xpcomf1o  6927  xpcomco  6928  dom0  6942  0dom  6943  xpmapenlem  6953  phplem2  6957  php5  6962  snnen2og  6963  1nen2  6965  php5dom  6967  ssfilem  6979  ssfiexmid  6980  domfiexmid  6982  0fin  6988  diffitest  6991  findcard  6992  findcard2  6993  findcard2s  6994  isinfinf  7001  ac6sfi  7002  inffiexmid  7010  pw1fin  7014  unfiexmid  7022  xpfi  7036  fisseneq  7038  ssfirab  7040  residfi  7049  en1eqsn  7057  snexxph  7059  sbthlem2  7067  sbthlemi3  7068  sbthlemi6  7071  sbthlem7  7072  fi0  7084  supeq1i  7097  infeq1i  7122  djuexb  7153  djuf1olemr  7163  inresflem  7169  djuinr  7172  updjudhcoinlf  7189  updjudhcoinrg  7190  casefun  7194  caserel  7196  caseinj  7198  caseinl  7200  caseinr  7201  omp1eomlem  7203  endjusym  7205  difinfsn  7209  difinfinf  7210  djuinj  7215  0ct  7216  ctmlemr  7217  ctssdclemn0  7219  ctssdccl  7220  omct  7226  ctfoex  7227  finomni  7249  exmidomni  7251  fodjuomni  7258  ctssexmid  7259  fodjumkv  7269  nninfwlporlem  7282  nninfwlpoimlemg  7284  nninfwlpoim  7288  nninfinfwlpo  7289  card0  7302  ficardon  7303  exmidonfinlem  7308  dju1p1e2  7312  exmidfodomrlemim  7316  exmidfodomrlemr  7317  exmidfodomrlemrALT  7318  3nelsucpw1  7353  sucpw1nss3  7354  3nsssucpw1  7355  2onetap  7374  exmidmotap  7380  0npi  7433  dmaddpi  7445  dmmulpi  7446  1lt2pi  7460  0nnq  7484  1nq  7486  dmaddpq  7499  dmmulpq  7500  rec1nq  7515  1lt2nq  7526  halfnqq  7530  prarloclemarch2  7539  enq0enq  7551  nqnq0pi  7558  nnnq0lem1  7566  addnnnq0  7569  mulnnnq0  7570  nq0m0r  7576  addpinq1  7584  prarloclem5  7620  prarloclemcalc  7622  1pr  7674  1idprl  7710  1idpru  7711  ltexprlemm  7720  recexprlem1ssl  7753  recexprlem1ssu  7754  suplocexprlemell  7833  suplocexprlem2b  7834  suplocexprlemmu  7838  suplocexprlemdisj  7840  suplocexprlemloc  7841  suplocexprlemub  7843  suplocexprlemlub  7844  prsrlem1  7862  addsrpr  7865  mulsrpr  7866  gt0srpr  7868  0nsr  7869  0r  7870  1sr  7871  m1r  7872  m1m1sr  7881  caucvgsr  7922  suplocsrlempr  7927  addresr  7957  mulresr  7958  pitonnlem1  7965  peano1nnnn  7972  axi2m1  7995  axcnre  8001  peano5nnnn  8012  axcaucvg  8020  mpomulf  8069  mulridi  8081  mullidi  8082  pnfnre  8121  mnfnre  8122  pnfnemnf  8134  mnfxr  8136  rexri  8137  ltnri  8172  ltleii  8182  00id  8220  addridi  8221  addlidi  8222  0cnALT  8269  negeqi  8273  negicn  8280  neg0  8325  renegcli  8341  negcli  8347  negidi  8348  negnegi  8349  subidi  8350  subid1i  8351  negne0bi  8352  negrebi  8353  mul02i  8469  mul01i  8470  mulm1i  8482  leidi  8565  gt0ne0ii  8567  inelr  8664  msqge0i  8697  gt0ap0ii  8708  1div1e1  8784  div1i  8820  eqnegi  8821  recclapi  8822  recidapi  8823  divmulapi  8846  rerecclapi  8857  redivclapi  8859  rerecapb  8923  recgt0  8930  ltp1i  8985  divgt0ii  8999  ltmul1ii  9008  ltdiv1ii  9009  sup3exmid  9037  peano5nni  9046  nnrei  9052  1nn  9054  nngt0i  9073  neg1ap0  9152  2timesi  9173  times2i  9174  2nn  9205  3nn  9206  4nn  9207  5nn  9208  6nn  9209  7nn  9210  8nn  9211  9nn  9212  2muline0  9269  rehalfcli  9293  nn0ssre  9306  nnnn0i  9310  dfn2  9315  0nn0  9317  nn0ge0i  9329  zrei  9385  neg1z  9411  nn0negzi  9414  dfz2  9452  nneoi  9484  peano5uzi  9489  dfuzi  9490  nn0ind-raph  9497  deceq1i  9517  deceq2i  9518  10nn  9526  numltc  9536  eluzel2  9660  eluz1i  9662  nn0uz  9690  nnuz  9691  infrenegsupex  9722  lbzbi  9744  divfnzn  9749  qdivcl  9771  irrmul  9775  irrmulap  9776  cnref1o  9779  0ltpnf  9911  mnflt0  9913  0lepnf  9919  xrltnsym  9922  xrlttri3  9926  nltpnft  9943  ngtmnft  9946  xrrebnd  9948  xnegmnf  9958  xneg0  9960  xltnegi  9964  xaddmnf1  9977  xaddmnf2  9978  mnfaddpnf  9980  xaddid1  9991  xnn0lenn0nn0  9994  xnn0xadd0  9996  xposdif  10011  ixxex  10028  iooval2  10044  unirnioo  10102  ioorebasg  10104  elrege0  10105  fzval2  10140  fzen  10172  fzprval  10211  fztpval  10212  uzdisj  10222  ige2m1fz  10239  fz01or  10240  fz1ssfz0  10246  fz0sn  10250  fz0tp  10251  fz0to3un2pr  10252  fz0to4untppr  10253  nn0disj  10267  1fv  10268  4fvwrd4  10269  fzo0ss1  10305  fzo01  10352  fzo12sn  10353  fzo0to2pr  10354  fzo0to3tp  10355  fzo0to42pr  10356  zsupssdc  10388  qbtwnxr  10407  flval  10422  fldiv4lem1div2  10457  modqfrac  10489  modqmulnn  10494  q2txmodxeq0  10536  frecuzrdgdom  10570  frecuzrdgfun  10572  frecuzrdgsuct  10576  frechashgf1o  10580  nnct  10587  xnn0nnen  10589  fxnn0nninf  10591  0tonninf  10592  1tonninf  10593  iseqvalcbv  10611  ser0f  10686  0exp0e1  10696  qexpcl  10707  qexpclz  10712  m1expcl2  10713  1exp  10720  sqvali  10771  sqcli  10772  sqeq0i  10773  resqcli  10776  sq1  10785  neg1sqe1  10786  iexpcyc  10796  qsqeqor  10802  facnn  10879  fac0  10880  fac1  10881  fac2  10883  fac3  10884  fac4  10885  bcval  10901  bcm1k  10912  bcpasc  10918  bccl  10919  4bc3eq4  10925  4bc2eq6  10926  hashinfom  10930  hashennn  10932  hashfz1  10935  fihasheq0  10945  hash0  10948  hashsng  10950  fihashen1  10951  omgadd  10954  hashp1i  10962  hashxp  10978  fimaxq  10979  zfz1iso  10993  hash2en  10995  wrdexi  11014  wrdv  11017  wrdeqi  11024  wrd0  11026  lsw0  11048  ccatclab  11058  ccatidid  11074  s1prc  11085  ccat1st1st  11101  swrds1  11129  shftidt2  11187  cjexp  11248  re0  11250  im0  11251  re1  11252  im1  11253  cj0  11256  cji  11257  recli  11266  imcli  11267  cjcli  11268  replimi  11269  cjcji  11270  reim0bi  11271  rerebi  11272  cjrebi  11273  recji  11274  imcji  11275  cjmulrcli  11276  cjmulvali  11277  cjmulge0i  11278  renegi  11279  imnegi  11280  cjnegi  11281  addcji  11282  uzin2  11342  rexanuz  11343  rexfiuz  11344  sqrtrval  11355  sqrt0  11359  resqrexlemcalc3  11371  resqrexlemcvg  11374  resqrex  11381  abs0  11413  absi  11414  qabsor  11430  absimle  11439  recan  11464  caubnd2  11472  leabsi  11483  absrei  11484  sqrtpclii  11485  sqrtgt0ii  11486  absvalsqi  11495  absvalsq2i  11496  abscli  11497  absge0i  11498  absval2i  11499  abs00i  11500  absgt0api  11501  absnegi  11502  abscji  11503  releabsi  11504  infxrnegsupex  11618  xrbdtri  11631  cbvsum  11715  sumeq1i  11718  sum0  11743  isumz  11744  fisumss  11747  fsumsersdc  11750  fsumadd  11761  isumclim  11776  isumclim3  11778  fsumcnv  11792  modfsummodlem1  11811  fsumrelem  11826  binomlem  11838  binom  11839  arisum2  11854  expcnv  11859  0.999...  11876  prodf1f  11898  cbvprod  11913  prodeq1i  11916  zproddc  11934  zprodap0  11936  prod0  11940  fprodssdc  11945  prodsnf  11947  fprodcnv  11980  fprodge0  11992  fprodge1  11994  ef0lem  12015  esum  12017  ere  12025  ege2le3  12026  ef0  12027  eff2  12035  efsep  12046  reeff1  12055  sin0  12084  cos0  12085  ef01bndlem  12111  cos2bnd  12115  sincos1sgn  12120  sincos2sgn  12121  sin4lt0  12122  eirr  12134  0dvds  12166  dvds1  12208  z0even  12266  n2dvdsm1  12268  z2even  12269  n2dvds3  12270  ndvdssub  12285  ndvdsi  12288  flodddiv4  12291  bits0  12303  bitsfzo  12310  0bits  12314  m1bits  12315  bitsinv1lem  12316  bitsinv1  12317  gcddvds  12328  gcd1  12352  6gcd4e2  12360  bezoutlembi  12370  dfgcd3  12375  dfgcd2  12379  nninfctlemfo  12405  nninfct  12406  3lcm2e6woprm  12452  qredeu  12463  isprm2lem  12482  isprm3  12484  prm2orodd  12492  isprm5lem  12507  sqrt2irr0  12530  pw2dvds  12532  phicl2  12580  phi1  12585  dfphi2  12586  phiprmpw  12588  eulerthlemrprm  12595  eulerthlemh  12597  odzval  12608  oddprm  12626  pczpre  12664  pcdiv  12669  pc0  12671  pcqdiv  12674  pcrec  12675  pcexp  12676  pcxcl  12678  pcxqcl  12679  pcdvdstr  12694  pc2dvds  12697  dvdsprmpweqnn  12703  pcmpt  12710  qexpz  12719  pockthi  12725  1arith2  12735  4sqlemffi  12763  4sqlem11  12768  4sqlem13m  12770  4sqlem19  12776  dec2dvds  12778  dec5nprm  12781  modxai  12783  modxp1i  12785  numexp0  12789  numexp1  12790  ennnfonelemp1  12821  ennnfonelem1  12822  ennnfonelemkh  12827  ennnfonelemex  12829  ennnfonelemnn0  12837  ennnfonelemr  12838  exmidunben  12841  ctinfomlemom  12842  ctinfom  12843  ctinf  12845  qnnen  12846  omctfn  12858  omiunct  12859  ssnnctlemct  12861  nninfdc  12868  structcnvcnv  12892  structfun  12894  structfn  12895  ndxarg  12899  ndxid  12900  setsresg  12914  setsslnid  12928  basmex  12935  basmexd  12936  strleun  12980  strle1g  12982  prdsex  13145  prdsvallem  13148  prdsval  13149  prdsbaslemss  13150  imasaddfnlemg  13190  quslem  13200  xpsfrnel  13220  xpsff1o  13225  ismgmn0  13234  fn0g  13251  0g0  13252  fngsum  13264  idghm  13639  rhmfn  13978  rmodislmodlem  14156  rmodislmod  14157  lidlmex  14281  mopnset  14358  cntopex  14360  cnfldex  14365  cnfldbas  14366  mpocnfldadd  14367  mpocnfldmul  14369  cnfldcj  14371  cnfldtset  14372  cnfldle  14373  cnfldds  14374  cnring  14376  cnfld0  14377  cnfld1  14378  cnfldneg  14379  cnfldplusf  14380  cnfldsub  14381  cnfldmulg  14382  cnfldexp  14383  cnsubglem  14385  cnsubrglem  14386  gzsubrg  14388  gsumfzfsumlem0  14392  cnfldui  14395  zringring  14399  zringabl  14400  zringgrp  14401  zring1  14407  zringsubgval  14411  expghmap  14413  znval  14442  znle  14443  znbaslemnn  14445  znbas  14450  znzrh2  14452  znzrhval  14453  znzrhfo  14454  znleval  14459  znidom  14463  znidomb  14464  fnpsr  14473  psrelbas  14481  psradd  14485  psraddcl  14486  psr1clfi  14494  mplrcl  14500  mplbasss  14502  mpladd  14510  istopon  14529  topontopi  14532  toponunii  14533  toponrestid  14537  istps  14548  topontopn  14553  eltpsi  14557  eltg4i  14571  eltg3  14573  tg1  14575  tg2  14576  tgclb  14581  topnex  14602  sn0topon  14604  distps  14607  cldrcl  14618  sn0cld  14653  restco  14690  lmrcl  14707  ssidcn  14726  cnconst2  14749  cnptopresti  14754  cnptoprest  14755  txuni2  14772  txbas  14774  eltx  14775  txcnp  14787  upxp  14788  txcnmpt  14789  uptx  14790  txcn  14791  txrest  14792  txlm  14795  cnmptid  14797  cnmpt1st  14804  cnmpt2nd  14805  hmeofn  14818  psmetge0  14847  ismeti  14862  xmetunirn  14874  xmetge0  14881  unirnblps  14938  unirnbl  14939  mopnex  15021  qtopbasss  15037  retop  15040  uniretop  15041  iooretopg  15044  cnxmet  15047  cntoptopon  15048  cnbl0  15050  cnfldxms  15053  cnfldtps  15054  rexmet  15065  blssioo  15069  tgioo  15070  tgqioo  15071  cnopnap  15127  hovercncf  15162  limcresi  15182  dvfvalap  15197  dvidlemap  15207  dvidrelem  15208  dvidsslem  15209  dvcnp2cntop  15215  dvcoapbr  15223  dvexp2  15228  dvrecap  15229  dveflem  15242  dvef  15243  plyun0  15252  plyrecj  15279  dvply2  15283  reeff1o  15289  sin0pilem1  15297  sin0pilem2  15298  pilem3  15299  pigt2lt4  15300  pire  15302  sinhalfpilem  15307  pidiv2halves  15311  cosneghalfpi  15314  cospi  15316  efipi  15317  sin2pi  15319  cos2pi  15320  ef2pi  15321  cosq14gt0  15348  coseq00topi  15351  coseq0negpitopi  15352  sincos4thpi  15356  sincos6thpi  15358  sincos3rdpi  15359  pigt3  15360  cos02pilt1  15367  ioocosf1o  15370  dfrelog  15376  relogf1o  15377  relogcl  15378  relogiso  15389  rpcxpsqrt  15438  rpabscxpbnd  15456  2logb9irr  15487  2logb9irrALT  15490  sqrt2cxp2logb9e3  15491  2irrexpq  15492  2logb9irrap  15493  2irrexpqap  15494  mpodvdsmulf1o  15506  fsumdvdsmul  15507  perfectlem2  15516  lgsdir2lem1  15549  lgsdir2lem2  15550  lgsdir2lem4  15552  lgsdir2lem5  15553  lgsdi  15558  gausslemma2dlem0i  15578  gausslemma2dlem4  15585  lgseisenlem4  15594  lgsquadlem1  15598  lgsquad2lem2  15603  lgsquad2  15604  m1lgs  15606  2lgs2  15623  2lgslem4  15624  2lgsoddprmlem2  15627  2lgsoddprmlem3c  15630  2lgsoddprmlem3d  15631  2sqlem9  15645  2sqlem10  15646  1vgrex  15663  vtxval0  15694  iedgval0  15695  uhgr0  15725  ex-fl  15735  ex-ceil  15736  ex-exp  15737  ex-fac  15738  ex-gcd  15741  bj-stfal  15752  bj-stst  15755  bj-dcfal  15765  bj-dcdc  15769  bj-stdc  15770  bj-dcst  15771  bj-el2oss1o  15784  elabf2  15792  bd0  15834  bdeli  15856  bdcriota  15893  bdbm1.3ii  15901  bdinex1  15909  bdssexi  15913  bj-inex  15917  bj-snex  15923  bj-sucex  15933  bj-d0clsepcl  15935  bj-omind  15944  bj-om  15947  bj-2inf  15948  bj-peano2  15949  bdpeano5  15953  bj-omssonALT  15973  bj-inf2vnlem1  15980  bj-omex2  15987  bj-nn0sucALT  15988  012of  16004  2o01f  16005  subctctexmid  16011  nninfall  16020  nninfsellemqall  16026  nninfsellemeqinf  16027  nninfomnilem  16029  nninfomni  16030  exmidsbthrlem  16035  sbthom  16039  isomninnlem  16043  isomninn  16044  cvgcmp2nlemabs  16045  iooreen  16048  trilpolemisumle  16051  trilpolemeq1  16053  trilpo  16056  trirec0  16057  apdifflemr  16060  iswomninnlem  16062  iswomninn  16063  ismkvnnlem  16065  ismkvnn  16066  redcwlpo  16068  dcapnconst  16074  nconstwlpolem0  16076  nconstwlpo  16079  neapmkv  16081  neap0mkv  16082  taupi  16086