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

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  669  nbn  700  ori  724  orci  732  olci  733  biorfi  747  imorri  750  dcbii  841  simp1i  1008  simp2i  1009  simp3i  1010  3mix1i  1171  3mix2i  1172  3mix3i  1173  3jaoi  1314  mptru  1373  dfnot  1382  mptnan  1434  mtpor  1436  mtpxor  1437  dcfromnotnotr  1458  dcfromcon  1459  dcfrompeirce  1460  mpg  1465  19.23h  1512  hbequid  1527  axi12  1528  nfri  1533  spi  1550  19.21  1597  eximii  1616  19.35i  1639  nfn  1672  19.37aiv  1689  19.23  1692  exan  1707  equid  1715  hbae  1732  equvini  1772  equveli  1773  sbid  1788  sbieh  1804  exdistrfor  1814  dveeq2or  1830  ax11v  1841  ax11ev  1842  equs5or  1844  sb4or  1847  sb4bor  1849  nfsb2or  1851  sbequilem  1852  sbequi  1853  speiv  1876  nfsbxy  1961  nfsbxyt  1962  sbco  1987  sbcocom  1989  sbcomxyyz  1991  sbal1yz  2020  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  eumoi  2078  moani  2115  elsb1  2174  elsb2  2175  eqeq1i  2204  eqeq2i  2207  eleq1i  2262  eleq2i  2263  nfcrii  2332  neeq1i  2382  neeq2i  2383  necon3i  2415  rspec  2549  rgen2a  2551  mprg  2554  r19.21  2573  r19.23  2605  raleqi  2697  rexeqi  2698  rabeqif  2754  elv  2767  elexi  2775  ceqsal  2792  vtocl3  2820  vtoclef  2837  vtocle  2838  spcv  2858  spcev  2859  clel3  2899  elabf  2907  elab2  2912  elab3  2916  euxfrdc  2950  reueq  2963  rmoimi2  2967  sbsbc  2993  sbc8g  2997  sbc6  3015  sbcie  3024  sbcrex  3069  csbvarg  3112  csbief  3129  csbie2  3134  sbnfc2  3145  sseli  3179  sselii  3180  sseq1i  3209  sseq2i  3210  difeq1i  3277  difeq2i  3278  uneq1i  3313  uneq2i  3314  ineq1i  3360  ineq2i  3361  ssinss1  3392  difdif2ss  3420  n0ii  3459  ne0ii  3460  vn0  3461  vn0m  3462  abf  3494  disj2  3506  difid  3519  0dif  3522  disjdif  3523  difin0  3524  undif1ss  3525  difdifdirss  3535  iftruei  3567  iffalsei  3570  ifbieq2i  3584  ifbieq12i  3586  pweqi  3609  pwid  3620  sneqi  3634  elsn  3638  elpr  3643  elsn2  3656  ralsn  3665  rexsn  3666  eltp  3670  rabrsndc  3690  preq1i  3702  preq2i  3703  prid1  3728  snnz  3741  snm  3742  prnz  3744  prm  3745  tpnz  3747  snss  3757  snsssn  3791  opeq1i  3811  opeq2i  3812  unieqi  3849  unissi  3862  inteqi  3878  intmin2  3900  intab  3903  intsn  3909  iinconstm  3925  iuniin  3926  iinss1  3928  iunxdif2  3965  ssiinf  3966  iinss  3968  iinss2  3969  iinab  3978  iundif2ss  3982  iindif2m  3984  iinin2m  3985  iunxsn  3993  iunxprg  3997  iinpw  4007  sndisj  4029  disjxsn  4031  breqi  4039  breq1i  4040  breq2i  4041  brab1  4080  opabbii  4100  truni  4145  bm1.3ii  4154  a9evsep  4155  ax9vsep  4156  zfnuleu  4157  axnul  4158  ssexi  4171  rabex  4177  rabex2  4179  elpw2  4190  pwnss  4192  iin0r  4202  intv  4203  pwex  4216  snex  4218  notnotsnex  4220  ord3ex  4223  dtruarb  4224  undifexmid  4226  intid  4257  opnzi  4268  copsexg  4277  opelopabf  4309  epelc  4326  elon  4409  inton  4428  onn0  4435  onm  4436  elsuc  4441  elsuc2  4442  sucid  4452  iunsuc  4455  onordi  4461  ontrci  4462  onelssi  4464  eusvnf  4488  ssonunii  4525  sucex  4535  onssi  4551  onsuci  4552  ordtriexmidlem  4555  ordtriexmidlem2  4556  ordtriexmid  4557  ontriexmidim  4558  ordtri2orexmid  4559  2ordpr  4560  ontr2exmid  4561  onsucsssucexmid  4563  onsucelsucexmid  4566  regexmidlemm  4568  reg2exmid  4572  onirri  4579  ruALT  4587  onprc  4588  sucon  4589  dtru  4596  0elsucexmid  4601  ordpwsucexmid  4606  ordtri2or2exmid  4607  ontri2orexmidim  4608  dcextest  4617  omex  4629  find  4635  omelon  4645  nnoni  4647  limom  4650  nnregexmid  4657  omsinds  4658  xpeq1i  4683  xpeq2i  4684  0nelxp  4691  opthprc  4714  mosubop  4729  releqi  4746  relssi  4754  relin1  4781  relin2  4782  reldif  4783  inopab  4798  difopab  4799  xpiindim  4803  opabbi2dv  4815  ideq  4818  coeq1i  4825  coeq2i  4826  cnveqi  4841  eldm  4863  eldm2  4864  dmeqi  4867  dmv  4882  rneqi  4894  elrnmpti  4919  dmex  4932  rnex  4933  reseq1i  4942  reseq2i  4943  residm  4978  resex  4987  resmpt3  4995  imaeq1i  5006  imaeq2i  5007  elima  5014  imaex  5024  elimasn  5036  args  5038  epini  5040  dfse2  5042  eliniseg2  5049  relbrcnv  5050  cotr  5051  issref  5052  cnvsym  5053  asymref  5055  intirr  5056  codir  5058  qfto  5059  ssrnres  5112  cnveq0  5126  cnvsn0  5138  dmsnop  5143  rnsnop  5150  resdm2  5160  dfco2a  5170  cocnvcnv1  5180  coi2  5186  coires1  5187  cnvssrndm  5191  cossxp  5192  cocnvres  5194  relrelss  5196  relcoi2  5200  unidmrn  5202  dfdm2  5204  unixpm  5205  cnvexg  5207  cnvex  5208  cnviinm  5211  iotaval  5230  funeqi  5279  funi  5290  funres  5299  funcnvsn  5303  funcnvcnv  5317  funin  5329  funcnvres  5331  isarep2  5345  fneq1i  5352  fneq2i  5353  fnresdisj  5368  fnresi  5375  mpt0  5385  dmmpti  5387  feq1i  5400  feq2i  5401  fdmi  5415  fun2  5431  fssres  5433  resasplitss  5437  fintm  5443  fconst6  5457  f1ores  5519  foimacnv  5522  resdif  5526  funcocnv2  5529  f1ovi  5543  fveq1i  5559  fveq2i  5561  0fv  5594  fvun1  5627  fvopab3ig  5635  fvmptss2  5636  mptrcl  5644  elfvmptrab1  5656  fndmdif  5667  fneqeql2  5671  f1oresrab  5727  fmptco  5728  fnressn  5748  fressnfv  5749  fmptap  5752  fvsnun1  5759  fvsnun2  5760  fsnunfv  5763  fconst2  5779  mptex  5788  riotabiia  5895  acexmidlema  5913  acexmidlemb  5914  acexmidlemcase  5917  acexmidlem2  5919  acexmidlemv  5920  oveq1i  5932  oveq2i  5933  oveqi  5935  oprabidlem  5953  0neqopab  5967  oprabbii  5977  oprabss  6008  mpompt  6014  funoprab  6022  fnoprab  6025  ovigg  6043  elmpocl  6118  resfunexgALT  6165  cofunexg  6166  mptexw  6170  opabex3d  6178  opabex3  6179  1st0  6202  2nd0  6203  op1st  6204  op2nd  6205  f1stres  6217  f2ndres  6218  fo1stresm  6219  fo2ndresm  6220  1stcof  6221  2ndcof  6222  1stexg  6225  2ndexg  6226  releldm2  6243  reldm  6244  dfoprab3  6249  mpomptsx  6255  mpompts  6256  fnmpoi  6261  dmmpo  6262  mpoexxg  6268  mpoexw  6271  1stconst  6279  2ndconst  6280  dfmpo  6281  algrflem  6287  algrflemg  6288  cnvoprab  6292  f1od2  6293  mpoxopn0yelv  6297  mpoxopoveq  6298  tposssxp  6307  brtpos2  6309  reldmtpos  6311  dftpos2  6319  dftpos4  6321  tpostpos  6322  tpostpos2  6323  tposfo  6329  tposf  6330  tposeqi  6335  tposex  6336  tposoprab  6338  issmo  6346  smores  6350  smores2  6352  iordsmo  6355  smo0  6356  tfrlem8  6376  tfrexlem  6392  tfr1onlem3  6396  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlemres  6407  tfri1dALT  6409  tfri2  6424  rdgisuc1  6442  rdg0  6445  frecfun  6453  frec0g  6455  freccllem  6460  frecfcllem  6462  frecsuclem  6464  frecrdg  6466  2on0  6484  xp01disj  6491  2oconcl  6497  fnoa  6505  oaexg  6506  fnom  6508  omexg  6509  fnoei  6510  oeiexg  6511  oei0  6517  oacl  6518  oasuc  6522  o1p1e2  6526  omsuc  6530  nna0r  6536  nnm0r  6537  1onn  6578  2onn  6579  3onn  6580  4onn  6581  2ssom  6582  eqerlem  6623  eceq2i  6630  elqs  6645  qsex  6651  ecqs  6656  iinerm  6666  th3qlem1  6696  th3q  6699  mapsn  6749  mapsnf1o3  6756  ixpiinm  6783  ixpssmap  6791  brdom  6809  f1dom  6819  enref  6824  dom2  6834  idssen  6836  ssdomg  6837  ensymi  6841  ensn1  6855  fiprc  6874  1domsn  6878  xpcomf1o  6884  xpcomco  6885  dom0  6899  0dom  6900  xpmapenlem  6910  phplem2  6914  php5  6919  snnen2og  6920  1nen2  6922  php5dom  6924  ssfilem  6936  ssfiexmid  6937  domfiexmid  6939  0fin  6945  diffitest  6948  findcard  6949  findcard2  6950  findcard2s  6951  isinfinf  6958  ac6sfi  6959  inffiexmid  6967  pw1fin  6971  unfiexmid  6979  xpfi  6993  fisseneq  6995  ssfirab  6997  residfi  7006  en1eqsn  7014  snexxph  7016  sbthlem2  7024  sbthlemi3  7025  sbthlemi6  7028  sbthlem7  7029  fi0  7041  supeq1i  7054  infeq1i  7079  djuexb  7110  djuf1olemr  7120  inresflem  7126  djuinr  7129  updjudhcoinlf  7146  updjudhcoinrg  7147  casefun  7151  caserel  7153  caseinj  7155  caseinl  7157  caseinr  7158  omp1eomlem  7160  endjusym  7162  difinfsn  7166  difinfinf  7167  djuinj  7172  0ct  7173  ctmlemr  7174  ctssdclemn0  7176  ctssdccl  7177  omct  7183  ctfoex  7184  finomni  7206  exmidomni  7208  fodjuomni  7215  ctssexmid  7216  fodjumkv  7226  nninfwlporlem  7239  nninfwlpoimlemg  7241  nninfwlpoim  7244  card0  7255  exmidonfinlem  7260  dju1p1e2  7264  exmidfodomrlemim  7268  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  3nelsucpw1  7301  sucpw1nss3  7302  3nsssucpw1  7303  2onetap  7322  exmidmotap  7328  0npi  7380  dmaddpi  7392  dmmulpi  7393  1lt2pi  7407  0nnq  7431  1nq  7433  dmaddpq  7446  dmmulpq  7447  rec1nq  7462  1lt2nq  7473  halfnqq  7477  prarloclemarch2  7486  enq0enq  7498  nqnq0pi  7505  nnnq0lem1  7513  addnnnq0  7516  mulnnnq0  7517  nq0m0r  7523  addpinq1  7531  prarloclem5  7567  prarloclemcalc  7569  1pr  7621  1idprl  7657  1idpru  7658  ltexprlemm  7667  recexprlem1ssl  7700  recexprlem1ssu  7701  suplocexprlemell  7780  suplocexprlem2b  7781  suplocexprlemmu  7785  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemub  7790  suplocexprlemlub  7791  prsrlem1  7809  addsrpr  7812  mulsrpr  7813  gt0srpr  7815  0nsr  7816  0r  7817  1sr  7818  m1r  7819  m1m1sr  7828  caucvgsr  7869  suplocsrlempr  7874  addresr  7904  mulresr  7905  pitonnlem1  7912  peano1nnnn  7919  axi2m1  7942  axcnre  7948  peano5nnnn  7959  axcaucvg  7967  mpomulf  8016  mulridi  8028  mullidi  8029  pnfnre  8068  mnfnre  8069  pnfnemnf  8081  mnfxr  8083  rexri  8084  ltnri  8119  ltleii  8129  00id  8167  addridi  8168  addlidi  8169  0cnALT  8216  negeqi  8220  negicn  8227  neg0  8272  renegcli  8288  negcli  8294  negidi  8295  negnegi  8296  subidi  8297  subid1i  8298  negne0bi  8299  negrebi  8300  mul02i  8416  mul01i  8417  mulm1i  8429  leidi  8512  gt0ne0ii  8514  inelr  8611  msqge0i  8644  gt0ap0ii  8655  1div1e1  8731  div1i  8767  eqnegi  8768  recclapi  8769  recidapi  8770  divmulapi  8793  rerecclapi  8804  redivclapi  8806  rerecapb  8870  recgt0  8877  ltp1i  8932  divgt0ii  8946  ltmul1ii  8955  ltdiv1ii  8956  sup3exmid  8984  peano5nni  8993  nnrei  8999  1nn  9001  nngt0i  9020  neg1ap0  9099  2timesi  9120  times2i  9121  2nn  9152  3nn  9153  4nn  9154  5nn  9155  6nn  9156  7nn  9157  8nn  9158  9nn  9159  2muline0  9216  rehalfcli  9240  nn0ssre  9253  nnnn0i  9257  dfn2  9262  0nn0  9264  nn0ge0i  9276  zrei  9332  neg1z  9358  nn0negzi  9361  dfz2  9398  nneoi  9430  peano5uzi  9435  dfuzi  9436  nn0ind-raph  9443  deceq1i  9463  deceq2i  9464  10nn  9472  numltc  9482  eluzel2  9606  eluz1i  9608  nn0uz  9636  nnuz  9637  infrenegsupex  9668  lbzbi  9690  divfnzn  9695  qdivcl  9717  irrmul  9721  irrmulap  9722  cnref1o  9725  0ltpnf  9857  mnflt0  9859  0lepnf  9865  xrltnsym  9868  xrlttri3  9872  nltpnft  9889  ngtmnft  9892  xrrebnd  9894  xnegmnf  9904  xneg0  9906  xltnegi  9910  xaddmnf1  9923  xaddmnf2  9924  mnfaddpnf  9926  xaddid1  9937  xnn0lenn0nn0  9940  xnn0xadd0  9942  xposdif  9957  ixxex  9974  iooval2  9990  unirnioo  10048  ioorebasg  10050  elrege0  10051  fzval2  10086  fzen  10118  fzprval  10157  fztpval  10158  uzdisj  10168  ige2m1fz  10185  fz01or  10186  fz1ssfz0  10192  fz0sn  10196  fz0tp  10197  fz0to3un2pr  10198  fz0to4untppr  10199  nn0disj  10213  1fv  10214  4fvwrd4  10215  fzo0ss1  10250  fzo01  10292  fzo12sn  10293  fzo0to2pr  10294  fzo0to3tp  10295  fzo0to42pr  10296  zsupssdc  10328  qbtwnxr  10347  flval  10362  fldiv4lem1div2  10397  modqfrac  10429  modqmulnn  10434  q2txmodxeq0  10476  frecuzrdgdom  10510  frecuzrdgfun  10512  frecuzrdgsuct  10516  frechashgf1o  10520  nnct  10527  xnn0nnen  10529  fxnn0nninf  10531  0tonninf  10532  1tonninf  10533  iseqvalcbv  10551  ser0f  10626  0exp0e1  10636  qexpcl  10647  qexpclz  10652  m1expcl2  10653  1exp  10660  sqvali  10711  sqcli  10712  sqeq0i  10713  resqcli  10716  sq1  10725  neg1sqe1  10726  iexpcyc  10736  qsqeqor  10742  facnn  10819  fac0  10820  fac1  10821  fac2  10823  fac3  10824  fac4  10825  bcval  10841  bcm1k  10852  bcpasc  10858  bccl  10859  4bc3eq4  10865  4bc2eq6  10866  hashinfom  10870  hashennn  10872  hashfz1  10875  fihasheq0  10885  hash0  10888  hashsng  10890  fihashen1  10891  omgadd  10894  hashp1i  10902  hashxp  10918  fimaxq  10919  zfz1iso  10933  wrdexi  10948  wrdv  10951  wrdeqi  10958  wrd0  10960  shftidt2  10997  cjexp  11058  re0  11060  im0  11061  re1  11062  im1  11063  cj0  11066  cji  11067  recli  11076  imcli  11077  cjcli  11078  replimi  11079  cjcji  11080  reim0bi  11081  rerebi  11082  cjrebi  11083  recji  11084  imcji  11085  cjmulrcli  11086  cjmulvali  11087  cjmulge0i  11088  renegi  11089  imnegi  11090  cjnegi  11091  addcji  11092  uzin2  11152  rexanuz  11153  rexfiuz  11154  sqrtrval  11165  sqrt0  11169  resqrexlemcalc3  11181  resqrexlemcvg  11184  resqrex  11191  abs0  11223  absi  11224  qabsor  11240  absimle  11249  recan  11274  caubnd2  11282  leabsi  11293  absrei  11294  sqrtpclii  11295  sqrtgt0ii  11296  absvalsqi  11305  absvalsq2i  11306  abscli  11307  absge0i  11308  absval2i  11309  abs00i  11310  absgt0api  11311  absnegi  11312  abscji  11313  releabsi  11314  infxrnegsupex  11428  xrbdtri  11441  cbvsum  11525  sumeq1i  11528  sum0  11553  isumz  11554  fisumss  11557  fsumsersdc  11560  fsumadd  11571  isumclim  11586  isumclim3  11588  fsumcnv  11602  modfsummodlem1  11621  fsumrelem  11636  binomlem  11648  binom  11649  arisum2  11664  expcnv  11669  0.999...  11686  prodf1f  11708  cbvprod  11723  prodeq1i  11726  zproddc  11744  zprodap0  11746  prod0  11750  fprodssdc  11755  prodsnf  11757  fprodcnv  11790  fprodge0  11802  fprodge1  11804  ef0lem  11825  esum  11827  ere  11835  ege2le3  11836  ef0  11837  eff2  11845  efsep  11856  reeff1  11865  sin0  11894  cos0  11895  ef01bndlem  11921  cos2bnd  11925  sincos1sgn  11930  sincos2sgn  11931  sin4lt0  11932  eirr  11944  0dvds  11976  dvds1  12018  z0even  12076  n2dvdsm1  12078  z2even  12079  n2dvds3  12080  ndvdssub  12095  ndvdsi  12098  flodddiv4  12101  bits0  12112  bitsfzo  12119  gcddvds  12130  gcd1  12154  6gcd4e2  12162  bezoutlembi  12172  dfgcd3  12177  dfgcd2  12181  nninfctlemfo  12207  nninfct  12208  3lcm2e6woprm  12254  qredeu  12265  isprm2lem  12284  isprm3  12286  prm2orodd  12294  isprm5lem  12309  sqrt2irr0  12332  pw2dvds  12334  phicl2  12382  phi1  12387  dfphi2  12388  phiprmpw  12390  eulerthlemrprm  12397  eulerthlemh  12399  odzval  12410  oddprm  12428  pczpre  12466  pcdiv  12471  pc0  12473  pcqdiv  12476  pcrec  12477  pcexp  12478  pcxcl  12480  pcxqcl  12481  pcdvdstr  12496  pc2dvds  12499  dvdsprmpweqnn  12505  pcmpt  12512  qexpz  12521  pockthi  12527  1arith2  12537  4sqlemffi  12565  4sqlem11  12570  4sqlem13m  12572  4sqlem19  12578  dec2dvds  12580  dec5nprm  12583  modxai  12585  modxp1i  12587  numexp0  12591  numexp1  12592  ennnfonelemp1  12623  ennnfonelem1  12624  ennnfonelemkh  12629  ennnfonelemex  12631  ennnfonelemnn0  12639  ennnfonelemr  12640  exmidunben  12643  ctinfomlemom  12644  ctinfom  12645  ctinf  12647  qnnen  12648  omctfn  12660  omiunct  12661  ssnnctlemct  12663  nninfdc  12670  structcnvcnv  12694  structfun  12696  structfn  12697  ndxarg  12701  ndxid  12702  setsresg  12716  setsslnid  12730  basmex  12737  basmexd  12738  strleun  12782  strle1g  12784  prdsex  12940  imasaddfnlemg  12957  quslem  12967  xpsfrnel  12987  xpsff1o  12992  ismgmn0  13001  fn0g  13018  0g0  13019  fngsum  13031  idghm  13389  rhmfn  13728  rmodislmodlem  13906  rmodislmod  13907  lidlmex  14031  mopnset  14108  cntopex  14110  cnfldex  14115  cnfldbas  14116  mpocnfldadd  14117  mpocnfldmul  14119  cnfldcj  14121  cnfldtset  14122  cnfldle  14123  cnfldds  14124  cnring  14126  cnfld0  14127  cnfld1  14128  cnfldneg  14129  cnfldplusf  14130  cnfldsub  14131  cnfldmulg  14132  cnfldexp  14133  cnsubglem  14135  cnsubrglem  14136  gzsubrg  14138  gsumfzfsumlem0  14142  cnfldui  14145  zringring  14149  zringabl  14150  zringgrp  14151  zring1  14157  zringsubgval  14161  expghmap  14163  znval  14192  znle  14193  znbaslemnn  14195  znbas  14200  znzrh2  14202  znzrhval  14203  znzrhfo  14204  znleval  14209  znidom  14213  znidomb  14214  fnpsr  14221  psrelbas  14228  psradd  14231  psraddcl  14232  istopon  14249  topontopi  14252  toponunii  14253  toponrestid  14257  istps  14268  topontopn  14273  eltpsi  14277  eltg4i  14291  eltg3  14293  tg1  14295  tg2  14296  tgclb  14301  topnex  14322  sn0topon  14324  distps  14327  cldrcl  14338  sn0cld  14373  restco  14410  lmrcl  14427  ssidcn  14446  cnconst2  14469  cnptopresti  14474  cnptoprest  14475  txuni2  14492  txbas  14494  eltx  14495  txcnp  14507  upxp  14508  txcnmpt  14509  uptx  14510  txcn  14511  txrest  14512  txlm  14515  cnmptid  14517  cnmpt1st  14524  cnmpt2nd  14525  hmeofn  14538  psmetge0  14567  ismeti  14582  xmetunirn  14594  xmetge0  14601  unirnblps  14658  unirnbl  14659  mopnex  14741  qtopbasss  14757  retop  14760  uniretop  14761  iooretopg  14764  cnxmet  14767  cntoptopon  14768  cnbl0  14770  cnfldxms  14773  cnfldtps  14774  rexmet  14785  blssioo  14789  tgioo  14790  tgqioo  14791  cnopnap  14847  hovercncf  14882  limcresi  14902  dvfvalap  14917  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvcnp2cntop  14935  dvcoapbr  14943  dvexp2  14948  dvrecap  14949  dveflem  14962  dvef  14963  plyun0  14972  plyrecj  14999  dvply2  15003  reeff1o  15009  sin0pilem1  15017  sin0pilem2  15018  pilem3  15019  pigt2lt4  15020  pire  15022  sinhalfpilem  15027  pidiv2halves  15031  cosneghalfpi  15034  cospi  15036  efipi  15037  sin2pi  15039  cos2pi  15040  ef2pi  15041  cosq14gt0  15068  coseq00topi  15071  coseq0negpitopi  15072  sincos4thpi  15076  sincos6thpi  15078  sincos3rdpi  15079  pigt3  15080  cos02pilt1  15087  ioocosf1o  15090  dfrelog  15096  relogf1o  15097  relogcl  15098  relogiso  15109  rpcxpsqrt  15158  rpabscxpbnd  15176  2logb9irr  15207  2logb9irrALT  15210  sqrt2cxp2logb9e3  15211  2irrexpq  15212  2logb9irrap  15213  2irrexpqap  15214  mpodvdsmulf1o  15226  fsumdvdsmul  15227  perfectlem2  15236  lgsdir2lem1  15269  lgsdir2lem2  15270  lgsdir2lem4  15272  lgsdir2lem5  15273  lgsdi  15278  gausslemma2dlem0i  15298  gausslemma2dlem4  15305  lgseisenlem4  15314  lgsquadlem1  15318  lgsquad2lem2  15323  lgsquad2  15324  m1lgs  15326  2lgs2  15343  2lgslem4  15344  2lgsoddprmlem2  15347  2lgsoddprmlem3c  15350  2lgsoddprmlem3d  15351  2sqlem9  15365  2sqlem10  15366  ex-fl  15371  ex-ceil  15372  ex-exp  15373  ex-fac  15374  ex-gcd  15377  bj-stfal  15388  bj-stst  15391  bj-dcfal  15401  bj-dcdc  15405  bj-stdc  15406  bj-dcst  15407  bj-el2oss1o  15420  elabf2  15428  bd0  15470  bdeli  15492  bdcriota  15529  bdbm1.3ii  15537  bdinex1  15545  bdssexi  15549  bj-inex  15553  bj-snex  15559  bj-sucex  15569  bj-d0clsepcl  15571  bj-omind  15580  bj-om  15583  bj-2inf  15584  bj-peano2  15585  bdpeano5  15589  bj-omssonALT  15609  bj-inf2vnlem1  15616  bj-omex2  15623  bj-nn0sucALT  15624  012of  15640  2o01f  15641  subctctexmid  15645  nninfall  15653  nninfsellemqall  15659  nninfsellemeqinf  15660  nninfomnilem  15662  nninfomni  15663  exmidsbthrlem  15666  sbthom  15670  isomninnlem  15674  isomninn  15675  cvgcmp2nlemabs  15676  iooreen  15679  trilpolemisumle  15682  trilpolemeq1  15684  trilpo  15687  trirec0  15688  apdifflemr  15691  iswomninnlem  15693  iswomninn  15694  ismkvnnlem  15696  ismkvnn  15697  redcwlpo  15699  dcapnconst  15705  nconstwlpolem0  15707  nconstwlpo  15710  neapmkv  15712  neap0mkv  15713  taupi  15717