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 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	⊢ 𝜑
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  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  1467  dcfromcon  1468  dcfrompeirce  1469  mpg  1474  19.23h  1521  hbequid  1536  axi12  1537  nfri  1542  spi  1559  19.21  1606  eximii  1625  19.35i  1648  nfn  1681  19.37aiv  1698  19.23  1701  exan  1716  equid  1724  hbae  1741  equvini  1781  equveli  1782  sbid  1797  sbieh  1813  exdistrfor  1823  dveeq2or  1839  ax11v  1850  ax11ev  1851  equs5or  1853  sb4or  1856  sb4bor  1858  nfsb2or  1860  sbequilem  1861  sbequi  1862  speiv  1885  nfsbxy  1970  nfsbxyt  1971  sbco  1996  sbcocom  1998  sbcomxyyz  2000  sbal1yz  2029  dvelimALT  2038  dvelimfv  2039  dvelimor  2046  eumoi  2087  moani  2124  elsb1  2183  elsb2  2184  eqeq1i  2213  eqeq2i  2216  eleq1i  2271  eleq2i  2272  nfcrii  2341  neeq1i  2391  neeq2i  2392  necon3i  2424  rspec  2558  rgen2a  2560  mprg  2563  r19.21  2582  r19.23  2614  raleqi  2706  rexeqi  2707  rabeqif  2763  elv  2776  elexi  2784  ceqsal  2801  vtocl3  2829  vtoclef  2846  vtocle  2847  spcv  2867  spcev  2868  clel3  2908  elabf  2916  elab2  2921  elab3  2925  euxfrdc  2959  reueq  2972  rmoimi2  2976  sbsbc  3002  sbc8g  3006  sbc6  3024  sbcie  3033  sbcrex  3078  csbvarg  3121  csbief  3138  csbie2  3143  sbnfc2  3154  sseli  3189  sselii  3190  sseq1i  3219  sseq2i  3220  difeq1i  3287  difeq2i  3288  uneq1i  3323  uneq2i  3324  ineq1i  3370  ineq2i  3371  ssinss1  3402  difdif2ss  3430  n0ii  3469  ne0ii  3470  vn0  3471  vn0m  3472  abf  3504  disj2  3516  difid  3529  0dif  3532  disjdif  3533  difin0  3534  undif1ss  3535  difdifdirss  3545  iftruei  3577  iffalsei  3580  ifbieq2i  3594  ifbieq12i  3596  pweqi  3620  pwid  3631  sneqi  3645  elsn  3649  elpr  3654  elsn2  3667  ralsn  3676  rexsn  3677  eltp  3681  rabrsndc  3701  preq1i  3713  preq2i  3714  prid1  3739  snnz  3752  snm  3753  prnz  3755  prm  3756  tpnz  3758  snss  3768  snsssn  3802  opeq1i  3822  opeq2i  3823  unieqi  3860  unissi  3873  inteqi  3889  intmin2  3911  intab  3914  intsn  3920  iinconstm  3936  iuniin  3937  iinss1  3939  iunxdif2  3976  ssiinf  3977  iinss  3979  iinss2  3980  iinab  3989  iundif2ss  3993  iindif2m  3995  iinin2m  3996  iunxsn  4004  iunxprg  4008  iinpw  4018  sndisj  4040  disjxsn  4042  breqi  4050  breq1i  4051  breq2i  4052  brab1  4091  opabbii  4111  truni  4156  bm1.3ii  4165  a9evsep  4166  ax9vsep  4167  zfnuleu  4168  axnul  4169  ssexi  4182  rabex  4188  rabex2  4190  elpw2  4201  pwnss  4203  iin0r  4213  intv  4214  pwex  4227  snex  4229  notnotsnex  4231  ord3ex  4234  dtruarb  4235  undifexmid  4237  intid  4268  opnzi  4279  copsexg  4288  opwo0id  4293  opelopabf  4321  epelc  4338  elon  4421  inton  4440  onn0  4447  onm  4448  elsuc  4453  elsuc2  4454  sucid  4464  iunsuc  4467  onordi  4473  ontrci  4474  onelssi  4476  eusvnf  4500  ssonunii  4537  sucex  4547  onssi  4563  onsuci  4564  ordtriexmidlem  4567  ordtriexmidlem2  4568  ordtriexmid  4569  ontriexmidim  4570  ordtri2orexmid  4571  2ordpr  4572  ontr2exmid  4573  onsucsssucexmid  4575  onsucelsucexmid  4578  regexmidlemm  4580  reg2exmid  4584  onirri  4591  ruALT  4599  onprc  4600  sucon  4601  dtru  4608  0elsucexmid  4613  ordpwsucexmid  4618  ordtri2or2exmid  4619  ontri2orexmidim  4620  dcextest  4629  omex  4641  find  4647  omelon  4657  nnoni  4659  limom  4662  nnregexmid  4669  omsinds  4670  xpeq1i  4695  xpeq2i  4696  0nelxp  4703  opthprc  4726  mosubop  4741  releqi  4758  relssi  4766  relin1  4793  relin2  4794  reldif  4795  inopab  4810  difopab  4811  xpiindim  4815  opabbi2dv  4827  ideq  4830  coeq1i  4837  coeq2i  4838  cnveqi  4853  eldm  4875  eldm2  4876  dmeqi  4879  dmv  4894  rneqi  4906  elrnmpti  4931  dmex  4945  rnex  4946  reseq1i  4955  reseq2i  4956  residm  4991  resex  5000  resmpt3  5008  imaeq1i  5019  imaeq2i  5020  elima  5027  imaex  5037  elimasn  5049  args  5051  epini  5053  dfse2  5055  eliniseg2  5062  relbrcnv  5063  cotr  5064  issref  5065  cnvsym  5066  asymref  5068  intirr  5069  codir  5071  qfto  5072  ssrnres  5125  cnveq0  5139  cnvsn0  5151  dmsnop  5156  rnsnop  5163  resdm2  5173  dfco2a  5183  cocnvcnv1  5193  coi2  5199  coires1  5200  cnvssrndm  5204  cossxp  5205  cocnvres  5207  relrelss  5209  relcoi2  5213  unidmrn  5215  dfdm2  5217  unixpm  5218  cnvexg  5220  cnvex  5221  cnviinm  5224  iotaval  5243  funeqi  5292  funi  5303  funres  5312  funcnvsn  5319  funcnvcnv  5333  funin  5345  funcnvres  5347  isarep2  5361  fneq1i  5368  fneq2i  5369  fndmi  5374  fnresdisj  5386  fnresi  5393  mpt0  5403  dmmpti  5405  feq1i  5418  feq2i  5419  fdmi  5433  fun2  5449  fssres  5451  resasplitss  5455  fintm  5461  fconst6  5475  f1ores  5537  foimacnv  5540  resdif  5544  funcocnv2  5547  f1ovi  5561  fveq1i  5577  fveq2i  5579  0fv  5612  fvun1  5645  fvopab3ig  5653  fvmptss2  5654  mptrcl  5662  elfvmptrab1  5674  fndmdif  5685  fneqeql2  5689  f1oresrab  5745  fmptco  5746  funopsn  5762  fnressn  5770  fressnfv  5771  fmptap  5774  fvsnun1  5781  fvsnun2  5782  fsnunfv  5785  fconst2  5801  mptex  5810  riotabiia  5917  acexmidlema  5935  acexmidlemb  5936  acexmidlemcase  5939  acexmidlem2  5941  acexmidlemv  5942  oveq1i  5954  oveq2i  5955  oveqi  5957  oprabidlem  5975  0neqopab  5990  oprabbii  6000  oprabss  6031  mpompt  6037  funoprab  6045  fnoprab  6048  ovigg  6066  elmpocl  6141  resfunexgALT  6193  cofunexg  6194  mptexw  6198  opabex3d  6206  opabex3  6207  1st0  6230  2nd0  6231  op1st  6232  op2nd  6233  f1stres  6245  f2ndres  6246  fo1stresm  6247  fo2ndresm  6248  1stcof  6249  2ndcof  6250  1stexg  6253  2ndexg  6254  releldm2  6271  reldm  6272  dfoprab3  6277  mpomptsx  6283  mpompts  6284  fnmpoi  6289  dmmpo  6290  mpoexxg  6296  mpoexw  6299  1stconst  6307  2ndconst  6308  dfmpo  6309  algrflem  6315  algrflemg  6316  cnvoprab  6320  f1od2  6321  mpoxopn0yelv  6325  mpoxopoveq  6326  tposssxp  6335  brtpos2  6337  reldmtpos  6339  dftpos2  6347  dftpos4  6349  tpostpos  6350  tpostpos2  6351  tposfo  6357  tposf  6358  tposeqi  6363  tposex  6364  tposoprab  6366  issmo  6374  smores  6378  smores2  6380  iordsmo  6383  smo0  6384  tfrlem8  6404  tfrexlem  6420  tfr1onlem3  6424  tfr1onlemsucaccv  6427  tfr1onlembxssdm  6429  tfr1onlemres  6435  tfri1dALT  6437  tfri2  6452  rdgisuc1  6470  rdg0  6473  frecfun  6481  frec0g  6483  freccllem  6488  frecfcllem  6490  frecsuclem  6492  frecrdg  6494  2on0  6512  xp01disj  6519  2oconcl  6525  fnoa  6533  oaexg  6534  fnom  6536  omexg  6537  fnoei  6538  oeiexg  6539  oei0  6545  oacl  6546  oasuc  6550  o1p1e2  6554  omsuc  6558  nna0r  6564  nnm0r  6565  1onn  6606  2onn  6607  3onn  6608  4onn  6609  2ssom  6610  eqerlem  6651  eceq2i  6658  elqs  6673  qsex  6679  ecqs  6684  iinerm  6694  th3qlem1  6724  th3q  6727  mapsn  6777  mapsnf1o3  6784  ixpiinm  6811  ixpssmap  6819  brdom  6839  f1dom  6851  enref  6856  dom2  6866  idssen  6868  ssdomg  6870  ensymi  6874  ensn1  6888  fiprc  6907  1domsn  6914  xpcomf1o  6920  xpcomco  6921  dom0  6935  0dom  6936  xpmapenlem  6946  phplem2  6950  php5  6955  snnen2og  6956  1nen2  6958  php5dom  6960  ssfilem  6972  ssfiexmid  6973  domfiexmid  6975  0fin  6981  diffitest  6984  findcard  6985  findcard2  6986  findcard2s  6987  isinfinf  6994  ac6sfi  6995  inffiexmid  7003  pw1fin  7007  unfiexmid  7015  xpfi  7029  fisseneq  7031  ssfirab  7033  residfi  7042  en1eqsn  7050  snexxph  7052  sbthlem2  7060  sbthlemi3  7061  sbthlemi6  7064  sbthlem7  7065  fi0  7077  supeq1i  7090  infeq1i  7115  djuexb  7146  djuf1olemr  7156  inresflem  7162  djuinr  7165  updjudhcoinlf  7182  updjudhcoinrg  7183  casefun  7187  caserel  7189  caseinj  7191  caseinl  7193  caseinr  7194  omp1eomlem  7196  endjusym  7198  difinfsn  7202  difinfinf  7203  djuinj  7208  0ct  7209  ctmlemr  7210  ctssdclemn0  7212  ctssdccl  7213  omct  7219  ctfoex  7220  finomni  7242  exmidomni  7244  fodjuomni  7251  ctssexmid  7252  fodjumkv  7262  nninfwlporlem  7275  nninfwlpoimlemg  7277  nninfwlpoim  7281  nninfinfwlpo  7282  card0  7295  ficardon  7296  exmidonfinlem  7301  dju1p1e2  7305  exmidfodomrlemim  7309  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  3nelsucpw1  7346  sucpw1nss3  7347  3nsssucpw1  7348  2onetap  7367  exmidmotap  7373  0npi  7426  dmaddpi  7438  dmmulpi  7439  1lt2pi  7453  0nnq  7477  1nq  7479  dmaddpq  7492  dmmulpq  7493  rec1nq  7508  1lt2nq  7519  halfnqq  7523  prarloclemarch2  7532  enq0enq  7544  nqnq0pi  7551  nnnq0lem1  7559  addnnnq0  7562  mulnnnq0  7563  nq0m0r  7569  addpinq1  7577  prarloclem5  7613  prarloclemcalc  7615  1pr  7667  1idprl  7703  1idpru  7704  ltexprlemm  7713  recexprlem1ssl  7746  recexprlem1ssu  7747  suplocexprlemell  7826  suplocexprlem2b  7827  suplocexprlemmu  7831  suplocexprlemdisj  7833  suplocexprlemloc  7834  suplocexprlemub  7836  suplocexprlemlub  7837  prsrlem1  7855  addsrpr  7858  mulsrpr  7859  gt0srpr  7861  0nsr  7862  0r  7863  1sr  7864  m1r  7865  m1m1sr  7874  caucvgsr  7915  suplocsrlempr  7920  addresr  7950  mulresr  7951  pitonnlem1  7958  peano1nnnn  7965  axi2m1  7988  axcnre  7994  peano5nnnn  8005  axcaucvg  8013  mpomulf  8062  mulridi  8074  mullidi  8075  pnfnre  8114  mnfnre  8115  pnfnemnf  8127  mnfxr  8129  rexri  8130  ltnri  8165  ltleii  8175  00id  8213  addridi  8214  addlidi  8215  0cnALT  8262  negeqi  8266  negicn  8273  neg0  8318  renegcli  8334  negcli  8340  negidi  8341  negnegi  8342  subidi  8343  subid1i  8344  negne0bi  8345  negrebi  8346  mul02i  8462  mul01i  8463  mulm1i  8475  leidi  8558  gt0ne0ii  8560  inelr  8657  msqge0i  8690  gt0ap0ii  8701  1div1e1  8777  div1i  8813  eqnegi  8814  recclapi  8815  recidapi  8816  divmulapi  8839  rerecclapi  8850  redivclapi  8852  rerecapb  8916  recgt0  8923  ltp1i  8978  divgt0ii  8992  ltmul1ii  9001  ltdiv1ii  9002  sup3exmid  9030  peano5nni  9039  nnrei  9045  1nn  9047  nngt0i  9066  neg1ap0  9145  2timesi  9166  times2i  9167  2nn  9198  3nn  9199  4nn  9200  5nn  9201  6nn  9202  7nn  9203  8nn  9204  9nn  9205  2muline0  9262  rehalfcli  9286  nn0ssre  9299  nnnn0i  9303  dfn2  9308  0nn0  9310  nn0ge0i  9322  zrei  9378  neg1z  9404  nn0negzi  9407  dfz2  9445  nneoi  9477  peano5uzi  9482  dfuzi  9483  nn0ind-raph  9490  deceq1i  9510  deceq2i  9511  10nn  9519  numltc  9529  eluzel2  9653  eluz1i  9655  nn0uz  9683  nnuz  9684  infrenegsupex  9715  lbzbi  9737  divfnzn  9742  qdivcl  9764  irrmul  9768  irrmulap  9769  cnref1o  9772  0ltpnf  9904  mnflt0  9906  0lepnf  9912  xrltnsym  9915  xrlttri3  9919  nltpnft  9936  ngtmnft  9939  xrrebnd  9941  xnegmnf  9951  xneg0  9953  xltnegi  9957  xaddmnf1  9970  xaddmnf2  9971  mnfaddpnf  9973  xaddid1  9984  xnn0lenn0nn0  9987  xnn0xadd0  9989  xposdif  10004  ixxex  10021  iooval2  10037  unirnioo  10095  ioorebasg  10097  elrege0  10098  fzval2  10133  fzen  10165  fzprval  10204  fztpval  10205  uzdisj  10215  ige2m1fz  10232  fz01or  10233  fz1ssfz0  10239  fz0sn  10243  fz0tp  10244  fz0to3un2pr  10245  fz0to4untppr  10246  nn0disj  10260  1fv  10261  4fvwrd4  10262  fzo0ss1  10298  fzo01  10345  fzo12sn  10346  fzo0to2pr  10347  fzo0to3tp  10348  fzo0to42pr  10349  zsupssdc  10381  qbtwnxr  10400  flval  10415  fldiv4lem1div2  10450  modqfrac  10482  modqmulnn  10487  q2txmodxeq0  10529  frecuzrdgdom  10563  frecuzrdgfun  10565  frecuzrdgsuct  10569  frechashgf1o  10573  nnct  10580  xnn0nnen  10582  fxnn0nninf  10584  0tonninf  10585  1tonninf  10586  iseqvalcbv  10604  ser0f  10679  0exp0e1  10689  qexpcl  10700  qexpclz  10705  m1expcl2  10706  1exp  10713  sqvali  10764  sqcli  10765  sqeq0i  10766  resqcli  10769  sq1  10778  neg1sqe1  10779  iexpcyc  10789  qsqeqor  10795  facnn  10872  fac0  10873  fac1  10874  fac2  10876  fac3  10877  fac4  10878  bcval  10894  bcm1k  10905  bcpasc  10911  bccl  10912  4bc3eq4  10918  4bc2eq6  10919  hashinfom  10923  hashennn  10925  hashfz1  10928  fihasheq0  10938  hash0  10941  hashsng  10943  fihashen1  10944  omgadd  10947  hashp1i  10955  hashxp  10971  fimaxq  10972  zfz1iso  10986  hash2en  10988  wrdexi  11007  wrdv  11010  wrdeqi  11017  wrd0  11019  lsw0  11041  ccatclab  11050  ccatidid  11066  s1prc  11077  ccat1st1st  11093  swrds1  11121  shftidt2  11143  cjexp  11204  re0  11206  im0  11207  re1  11208  im1  11209  cj0  11212  cji  11213  recli  11222  imcli  11223  cjcli  11224  replimi  11225  cjcji  11226  reim0bi  11227  rerebi  11228  cjrebi  11229  recji  11230  imcji  11231  cjmulrcli  11232  cjmulvali  11233  cjmulge0i  11234  renegi  11235  imnegi  11236  cjnegi  11237  addcji  11238  uzin2  11298  rexanuz  11299  rexfiuz  11300  sqrtrval  11311  sqrt0  11315  resqrexlemcalc3  11327  resqrexlemcvg  11330  resqrex  11337  abs0  11369  absi  11370  qabsor  11386  absimle  11395  recan  11420  caubnd2  11428  leabsi  11439  absrei  11440  sqrtpclii  11441  sqrtgt0ii  11442  absvalsqi  11451  absvalsq2i  11452  abscli  11453  absge0i  11454  absval2i  11455  abs00i  11456  absgt0api  11457  absnegi  11458  abscji  11459  releabsi  11460  infxrnegsupex  11574  xrbdtri  11587  cbvsum  11671  sumeq1i  11674  sum0  11699  isumz  11700  fisumss  11703  fsumsersdc  11706  fsumadd  11717  isumclim  11732  isumclim3  11734  fsumcnv  11748  modfsummodlem1  11767  fsumrelem  11782  binomlem  11794  binom  11795  arisum2  11810  expcnv  11815  0.999...  11832  prodf1f  11854  cbvprod  11869  prodeq1i  11872  zproddc  11890  zprodap0  11892  prod0  11896  fprodssdc  11901  prodsnf  11903  fprodcnv  11936  fprodge0  11948  fprodge1  11950  ef0lem  11971  esum  11973  ere  11981  ege2le3  11982  ef0  11983  eff2  11991  efsep  12002  reeff1  12011  sin0  12040  cos0  12041  ef01bndlem  12067  cos2bnd  12071  sincos1sgn  12076  sincos2sgn  12077  sin4lt0  12078  eirr  12090  0dvds  12122  dvds1  12164  z0even  12222  n2dvdsm1  12224  z2even  12225  n2dvds3  12226  ndvdssub  12241  ndvdsi  12244  flodddiv4  12247  bits0  12259  bitsfzo  12266  0bits  12270  m1bits  12271  bitsinv1lem  12272  bitsinv1  12273  gcddvds  12284  gcd1  12308  6gcd4e2  12316  bezoutlembi  12326  dfgcd3  12331  dfgcd2  12335  nninfctlemfo  12361  nninfct  12362  3lcm2e6woprm  12408  qredeu  12419  isprm2lem  12438  isprm3  12440  prm2orodd  12448  isprm5lem  12463  sqrt2irr0  12486  pw2dvds  12488  phicl2  12536  phi1  12541  dfphi2  12542  phiprmpw  12544  eulerthlemrprm  12551  eulerthlemh  12553  odzval  12564  oddprm  12582  pczpre  12620  pcdiv  12625  pc0  12627  pcqdiv  12630  pcrec  12631  pcexp  12632  pcxcl  12634  pcxqcl  12635  pcdvdstr  12650  pc2dvds  12653  dvdsprmpweqnn  12659  pcmpt  12666  qexpz  12675  pockthi  12681  1arith2  12691  4sqlemffi  12719  4sqlem11  12724  4sqlem13m  12726  4sqlem19  12732  dec2dvds  12734  dec5nprm  12737  modxai  12739  modxp1i  12741  numexp0  12745  numexp1  12746  ennnfonelemp1  12777  ennnfonelem1  12778  ennnfonelemkh  12783  ennnfonelemex  12785  ennnfonelemnn0  12793  ennnfonelemr  12794  exmidunben  12797  ctinfomlemom  12798  ctinfom  12799  ctinf  12801  qnnen  12802  omctfn  12814  omiunct  12815  ssnnctlemct  12817  nninfdc  12824  structcnvcnv  12848  structfun  12850  structfn  12851  ndxarg  12855  ndxid  12856  setsresg  12870  setsslnid  12884  basmex  12891  basmexd  12892  strleun  12936  strle1g  12938  prdsex  13101  prdsvallem  13104  prdsval  13105  prdsbaslemss  13106  imasaddfnlemg  13146  quslem  13156  xpsfrnel  13176  xpsff1o  13181  ismgmn0  13190  fn0g  13207  0g0  13208  fngsum  13220  idghm  13595  rhmfn  13934  rmodislmodlem  14112  rmodislmod  14113  lidlmex  14237  mopnset  14314  cntopex  14316  cnfldex  14321  cnfldbas  14322  mpocnfldadd  14323  mpocnfldmul  14325  cnfldcj  14327  cnfldtset  14328  cnfldle  14329  cnfldds  14330  cnring  14332  cnfld0  14333  cnfld1  14334  cnfldneg  14335  cnfldplusf  14336  cnfldsub  14337  cnfldmulg  14338  cnfldexp  14339  cnsubglem  14341  cnsubrglem  14342  gzsubrg  14344  gsumfzfsumlem0  14348  cnfldui  14351  zringring  14355  zringabl  14356  zringgrp  14357  zring1  14363  zringsubgval  14367  expghmap  14369  znval  14398  znle  14399  znbaslemnn  14401  znbas  14406  znzrh2  14408  znzrhval  14409  znzrhfo  14410  znleval  14415  znidom  14419  znidomb  14420  fnpsr  14429  psrelbas  14437  psradd  14441  psraddcl  14442  psr1clfi  14450  mplrcl  14456  mplbasss  14458  mpladd  14466  istopon  14485  topontopi  14488  toponunii  14489  toponrestid  14493  istps  14504  topontopn  14509  eltpsi  14513  eltg4i  14527  eltg3  14529  tg1  14531  tg2  14532  tgclb  14537  topnex  14558  sn0topon  14560  distps  14563  cldrcl  14574  sn0cld  14609  restco  14646  lmrcl  14663  ssidcn  14682  cnconst2  14705  cnptopresti  14710  cnptoprest  14711  txuni2  14728  txbas  14730  eltx  14731  txcnp  14743  upxp  14744  txcnmpt  14745  uptx  14746  txcn  14747  txrest  14748  txlm  14751  cnmptid  14753  cnmpt1st  14760  cnmpt2nd  14761  hmeofn  14774  psmetge0  14803  ismeti  14818  xmetunirn  14830  xmetge0  14837  unirnblps  14894  unirnbl  14895  mopnex  14977  qtopbasss  14993  retop  14996  uniretop  14997  iooretopg  15000  cnxmet  15003  cntoptopon  15004  cnbl0  15006  cnfldxms  15009  cnfldtps  15010  rexmet  15021  blssioo  15025  tgioo  15026  tgqioo  15027  cnopnap  15083  hovercncf  15118  limcresi  15138  dvfvalap  15153  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvcnp2cntop  15171  dvcoapbr  15179  dvexp2  15184  dvrecap  15185  dveflem  15198  dvef  15199  plyun0  15208  plyrecj  15235  dvply2  15239  reeff1o  15245  sin0pilem1  15253  sin0pilem2  15254  pilem3  15255  pigt2lt4  15256  pire  15258  sinhalfpilem  15263  pidiv2halves  15267  cosneghalfpi  15270  cospi  15272  efipi  15273  sin2pi  15275  cos2pi  15276  ef2pi  15277  cosq14gt0  15304  coseq00topi  15307  coseq0negpitopi  15308  sincos4thpi  15312  sincos6thpi  15314  sincos3rdpi  15315  pigt3  15316  cos02pilt1  15323  ioocosf1o  15326  dfrelog  15332  relogf1o  15333  relogcl  15334  relogiso  15345  rpcxpsqrt  15394  rpabscxpbnd  15412  2logb9irr  15443  2logb9irrALT  15446  sqrt2cxp2logb9e3  15447  2irrexpq  15448  2logb9irrap  15449  2irrexpqap  15450  mpodvdsmulf1o  15462  fsumdvdsmul  15463  perfectlem2  15472  lgsdir2lem1  15505  lgsdir2lem2  15506  lgsdir2lem4  15508  lgsdir2lem5  15509  lgsdi  15514  gausslemma2dlem0i  15534  gausslemma2dlem4  15541  lgseisenlem4  15550  lgsquadlem1  15554  lgsquad2lem2  15559  lgsquad2  15560  m1lgs  15562  2lgs2  15579  2lgslem4  15580  2lgsoddprmlem2  15583  2lgsoddprmlem3c  15586  2lgsoddprmlem3d  15587  2sqlem9  15601  2sqlem10  15602  1vgrex  15617  vtxval0  15648  iedgval0  15649  ex-fl  15661  ex-ceil  15662  ex-exp  15663  ex-fac  15664  ex-gcd  15667  bj-stfal  15678  bj-stst  15681  bj-dcfal  15691  bj-dcdc  15695  bj-stdc  15696  bj-dcst  15697  bj-el2oss1o  15710  elabf2  15718  bd0  15760  bdeli  15782  bdcriota  15819  bdbm1.3ii  15827  bdinex1  15835  bdssexi  15839  bj-inex  15843  bj-snex  15849  bj-sucex  15859  bj-d0clsepcl  15861  bj-omind  15870  bj-om  15873  bj-2inf  15874  bj-peano2  15875  bdpeano5  15879  bj-omssonALT  15899  bj-inf2vnlem1  15906  bj-omex2  15913  bj-nn0sucALT  15914  012of  15930  2o01f  15931  subctctexmid  15937  nninfall  15946  nninfsellemqall  15952  nninfsellemeqinf  15953  nninfomnilem  15955  nninfomni  15956  exmidsbthrlem  15961  sbthom  15965  isomninnlem  15969  isomninn  15970  cvgcmp2nlemabs  15971  iooreen  15974  trilpolemisumle  15977  trilpolemeq1  15979  trilpo  15982  trirec0  15983  apdifflemr  15986  iswomninnlem  15988  iswomninn  15989  ismkvnnlem  15991  ismkvnn  15992  redcwlpo  15994  dcapnconst  16000  nconstwlpolem0  16002  nconstwlpo  16005  neapmkv  16007  neap0mkv  16008  taupi  16012