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 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	|- 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  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  3180  sselii  3181  sseq1i  3210  sseq2i  3211  difeq1i  3278  difeq2i  3279  uneq1i  3314  uneq2i  3315  ineq1i  3361  ineq2i  3362  ssinss1  3393  difdif2ss  3421  n0ii  3460  ne0ii  3461  vn0  3462  vn0m  3463  abf  3495  disj2  3507  difid  3520  0dif  3523  disjdif  3524  difin0  3525  undif1ss  3526  difdifdirss  3536  iftruei  3568  iffalsei  3571  ifbieq2i  3585  ifbieq12i  3587  pweqi  3610  pwid  3621  sneqi  3635  elsn  3639  elpr  3644  elsn2  3657  ralsn  3666  rexsn  3667  eltp  3671  rabrsndc  3691  preq1i  3703  preq2i  3704  prid1  3729  snnz  3742  snm  3743  prnz  3745  prm  3746  tpnz  3748  snss  3758  snsssn  3792  opeq1i  3812  opeq2i  3813  unieqi  3850  unissi  3863  inteqi  3879  intmin2  3901  intab  3904  intsn  3910  iinconstm  3926  iuniin  3927  iinss1  3929  iunxdif2  3966  ssiinf  3967  iinss  3969  iinss2  3970  iinab  3979  iundif2ss  3983  iindif2m  3985  iinin2m  3986  iunxsn  3994  iunxprg  3998  iinpw  4008  sndisj  4030  disjxsn  4032  breqi  4040  breq1i  4041  breq2i  4042  brab1  4081  opabbii  4101  truni  4146  bm1.3ii  4155  a9evsep  4156  ax9vsep  4157  zfnuleu  4158  axnul  4159  ssexi  4172  rabex  4178  rabex2  4180  elpw2  4191  pwnss  4193  iin0r  4203  intv  4204  pwex  4217  snex  4219  notnotsnex  4221  ord3ex  4224  dtruarb  4225  undifexmid  4227  intid  4258  opnzi  4269  copsexg  4278  opelopabf  4310  epelc  4327  elon  4410  inton  4429  onn0  4436  onm  4437  elsuc  4442  elsuc2  4443  sucid  4453  iunsuc  4456  onordi  4462  ontrci  4463  onelssi  4465  eusvnf  4489  ssonunii  4526  sucex  4536  onssi  4552  onsuci  4553  ordtriexmidlem  4556  ordtriexmidlem2  4557  ordtriexmid  4558  ontriexmidim  4559  ordtri2orexmid  4560  2ordpr  4561  ontr2exmid  4562  onsucsssucexmid  4564  onsucelsucexmid  4567  regexmidlemm  4569  reg2exmid  4573  onirri  4580  ruALT  4588  onprc  4589  sucon  4590  dtru  4597  0elsucexmid  4602  ordpwsucexmid  4607  ordtri2or2exmid  4608  ontri2orexmidim  4609  dcextest  4618  omex  4630  find  4636  omelon  4646  nnoni  4648  limom  4651  nnregexmid  4658  omsinds  4659  xpeq1i  4684  xpeq2i  4685  0nelxp  4692  opthprc  4715  mosubop  4730  releqi  4747  relssi  4755  relin1  4782  relin2  4783  reldif  4784  inopab  4799  difopab  4800  xpiindim  4804  opabbi2dv  4816  ideq  4819  coeq1i  4826  coeq2i  4827  cnveqi  4842  eldm  4864  eldm2  4865  dmeqi  4868  dmv  4883  rneqi  4895  elrnmpti  4920  dmex  4933  rnex  4934  reseq1i  4943  reseq2i  4944  residm  4979  resex  4988  resmpt3  4996  imaeq1i  5007  imaeq2i  5008  elima  5015  imaex  5025  elimasn  5037  args  5039  epini  5041  dfse2  5043  eliniseg2  5050  relbrcnv  5051  cotr  5052  issref  5053  cnvsym  5054  asymref  5056  intirr  5057  codir  5059  qfto  5060  ssrnres  5113  cnveq0  5127  cnvsn0  5139  dmsnop  5144  rnsnop  5151  resdm2  5161  dfco2a  5171  cocnvcnv1  5181  coi2  5187  coires1  5188  cnvssrndm  5192  cossxp  5193  cocnvres  5195  relrelss  5197  relcoi2  5201  unidmrn  5203  dfdm2  5205  unixpm  5206  cnvexg  5208  cnvex  5209  cnviinm  5212  iotaval  5231  funeqi  5280  funi  5291  funres  5300  funcnvsn  5304  funcnvcnv  5318  funin  5330  funcnvres  5332  isarep2  5346  fneq1i  5353  fneq2i  5354  fndmi  5359  fnresdisj  5371  fnresi  5378  mpt0  5388  dmmpti  5390  feq1i  5403  feq2i  5404  fdmi  5418  fun2  5434  fssres  5436  resasplitss  5440  fintm  5446  fconst6  5460  f1ores  5522  foimacnv  5525  resdif  5529  funcocnv2  5532  f1ovi  5546  fveq1i  5562  fveq2i  5564  0fv  5597  fvun1  5630  fvopab3ig  5638  fvmptss2  5639  mptrcl  5647  elfvmptrab1  5659  fndmdif  5670  fneqeql2  5674  f1oresrab  5730  fmptco  5731  fnressn  5751  fressnfv  5752  fmptap  5755  fvsnun1  5762  fvsnun2  5763  fsnunfv  5766  fconst2  5782  mptex  5791  riotabiia  5898  acexmidlema  5916  acexmidlemb  5917  acexmidlemcase  5920  acexmidlem2  5922  acexmidlemv  5923  oveq1i  5935  oveq2i  5936  oveqi  5938  oprabidlem  5956  0neqopab  5971  oprabbii  5981  oprabss  6012  mpompt  6018  funoprab  6026  fnoprab  6029  ovigg  6047  elmpocl  6122  resfunexgALT  6174  cofunexg  6175  mptexw  6179  opabex3d  6187  opabex3  6188  1st0  6211  2nd0  6212  op1st  6213  op2nd  6214  f1stres  6226  f2ndres  6227  fo1stresm  6228  fo2ndresm  6229  1stcof  6230  2ndcof  6231  1stexg  6234  2ndexg  6235  releldm2  6252  reldm  6253  dfoprab3  6258  mpomptsx  6264  mpompts  6265  fnmpoi  6270  dmmpo  6271  mpoexxg  6277  mpoexw  6280  1stconst  6288  2ndconst  6289  dfmpo  6290  algrflem  6296  algrflemg  6297  cnvoprab  6301  f1od2  6302  mpoxopn0yelv  6306  mpoxopoveq  6307  tposssxp  6316  brtpos2  6318  reldmtpos  6320  dftpos2  6328  dftpos4  6330  tpostpos  6331  tpostpos2  6332  tposfo  6338  tposf  6339  tposeqi  6344  tposex  6345  tposoprab  6347  issmo  6355  smores  6359  smores2  6361  iordsmo  6364  smo0  6365  tfrlem8  6385  tfrexlem  6401  tfr1onlem3  6405  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlemres  6416  tfri1dALT  6418  tfri2  6433  rdgisuc1  6451  rdg0  6454  frecfun  6462  frec0g  6464  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecrdg  6475  2on0  6493  xp01disj  6500  2oconcl  6506  fnoa  6514  oaexg  6515  fnom  6517  omexg  6518  fnoei  6519  oeiexg  6520  oei0  6526  oacl  6527  oasuc  6531  o1p1e2  6535  omsuc  6539  nna0r  6545  nnm0r  6546  1onn  6587  2onn  6588  3onn  6589  4onn  6590  2ssom  6591  eqerlem  6632  eceq2i  6639  elqs  6654  qsex  6660  ecqs  6665  iinerm  6675  th3qlem1  6705  th3q  6708  mapsn  6758  mapsnf1o3  6765  ixpiinm  6792  ixpssmap  6800  brdom  6818  f1dom  6828  enref  6833  dom2  6843  idssen  6845  ssdomg  6846  ensymi  6850  ensn1  6864  fiprc  6883  1domsn  6887  xpcomf1o  6893  xpcomco  6894  dom0  6908  0dom  6909  xpmapenlem  6919  phplem2  6923  php5  6928  snnen2og  6929  1nen2  6931  php5dom  6933  ssfilem  6945  ssfiexmid  6946  domfiexmid  6948  0fin  6954  diffitest  6957  findcard  6958  findcard2  6959  findcard2s  6960  isinfinf  6967  ac6sfi  6968  inffiexmid  6976  pw1fin  6980  unfiexmid  6988  xpfi  7002  fisseneq  7004  ssfirab  7006  residfi  7015  en1eqsn  7023  snexxph  7025  sbthlem2  7033  sbthlemi3  7034  sbthlemi6  7037  sbthlem7  7038  fi0  7050  supeq1i  7063  infeq1i  7088  djuexb  7119  djuf1olemr  7129  inresflem  7135  djuinr  7138  updjudhcoinlf  7155  updjudhcoinrg  7156  casefun  7160  caserel  7162  caseinj  7164  caseinl  7166  caseinr  7167  omp1eomlem  7169  endjusym  7171  difinfsn  7175  difinfinf  7176  djuinj  7181  0ct  7182  ctmlemr  7183  ctssdclemn0  7185  ctssdccl  7186  omct  7192  ctfoex  7193  finomni  7215  exmidomni  7217  fodjuomni  7224  ctssexmid  7225  fodjumkv  7235  nninfwlporlem  7248  nninfwlpoimlemg  7250  nninfwlpoim  7253  card0  7266  ficardon  7267  exmidonfinlem  7272  dju1p1e2  7276  exmidfodomrlemim  7280  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  3nelsucpw1  7317  sucpw1nss3  7318  3nsssucpw1  7319  2onetap  7338  exmidmotap  7344  0npi  7397  dmaddpi  7409  dmmulpi  7410  1lt2pi  7424  0nnq  7448  1nq  7450  dmaddpq  7463  dmmulpq  7464  rec1nq  7479  1lt2nq  7490  halfnqq  7494  prarloclemarch2  7503  enq0enq  7515  nqnq0pi  7522  nnnq0lem1  7530  addnnnq0  7533  mulnnnq0  7534  nq0m0r  7540  addpinq1  7548  prarloclem5  7584  prarloclemcalc  7586  1pr  7638  1idprl  7674  1idpru  7675  ltexprlemm  7684  recexprlem1ssl  7717  recexprlem1ssu  7718  suplocexprlemell  7797  suplocexprlem2b  7798  suplocexprlemmu  7802  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemub  7807  suplocexprlemlub  7808  prsrlem1  7826  addsrpr  7829  mulsrpr  7830  gt0srpr  7832  0nsr  7833  0r  7834  1sr  7835  m1r  7836  m1m1sr  7845  caucvgsr  7886  suplocsrlempr  7891  addresr  7921  mulresr  7922  pitonnlem1  7929  peano1nnnn  7936  axi2m1  7959  axcnre  7965  peano5nnnn  7976  axcaucvg  7984  mpomulf  8033  mulridi  8045  mullidi  8046  pnfnre  8085  mnfnre  8086  pnfnemnf  8098  mnfxr  8100  rexri  8101  ltnri  8136  ltleii  8146  00id  8184  addridi  8185  addlidi  8186  0cnALT  8233  negeqi  8237  negicn  8244  neg0  8289  renegcli  8305  negcli  8311  negidi  8312  negnegi  8313  subidi  8314  subid1i  8315  negne0bi  8316  negrebi  8317  mul02i  8433  mul01i  8434  mulm1i  8446  leidi  8529  gt0ne0ii  8531  inelr  8628  msqge0i  8661  gt0ap0ii  8672  1div1e1  8748  div1i  8784  eqnegi  8785  recclapi  8786  recidapi  8787  divmulapi  8810  rerecclapi  8821  redivclapi  8823  rerecapb  8887  recgt0  8894  ltp1i  8949  divgt0ii  8963  ltmul1ii  8972  ltdiv1ii  8973  sup3exmid  9001  peano5nni  9010  nnrei  9016  1nn  9018  nngt0i  9037  neg1ap0  9116  2timesi  9137  times2i  9138  2nn  9169  3nn  9170  4nn  9171  5nn  9172  6nn  9173  7nn  9174  8nn  9175  9nn  9176  2muline0  9233  rehalfcli  9257  nn0ssre  9270  nnnn0i  9274  dfn2  9279  0nn0  9281  nn0ge0i  9293  zrei  9349  neg1z  9375  nn0negzi  9378  dfz2  9415  nneoi  9447  peano5uzi  9452  dfuzi  9453  nn0ind-raph  9460  deceq1i  9480  deceq2i  9481  10nn  9489  numltc  9499  eluzel2  9623  eluz1i  9625  nn0uz  9653  nnuz  9654  infrenegsupex  9685  lbzbi  9707  divfnzn  9712  qdivcl  9734  irrmul  9738  irrmulap  9739  cnref1o  9742  0ltpnf  9874  mnflt0  9876  0lepnf  9882  xrltnsym  9885  xrlttri3  9889  nltpnft  9906  ngtmnft  9909  xrrebnd  9911  xnegmnf  9921  xneg0  9923  xltnegi  9927  xaddmnf1  9940  xaddmnf2  9941  mnfaddpnf  9943  xaddid1  9954  xnn0lenn0nn0  9957  xnn0xadd0  9959  xposdif  9974  ixxex  9991  iooval2  10007  unirnioo  10065  ioorebasg  10067  elrege0  10068  fzval2  10103  fzen  10135  fzprval  10174  fztpval  10175  uzdisj  10185  ige2m1fz  10202  fz01or  10203  fz1ssfz0  10209  fz0sn  10213  fz0tp  10214  fz0to3un2pr  10215  fz0to4untppr  10216  nn0disj  10230  1fv  10231  4fvwrd4  10232  fzo0ss1  10267  fzo01  10309  fzo12sn  10310  fzo0to2pr  10311  fzo0to3tp  10312  fzo0to42pr  10313  zsupssdc  10345  qbtwnxr  10364  flval  10379  fldiv4lem1div2  10414  modqfrac  10446  modqmulnn  10451  q2txmodxeq0  10493  frecuzrdgdom  10527  frecuzrdgfun  10529  frecuzrdgsuct  10533  frechashgf1o  10537  nnct  10544  xnn0nnen  10546  fxnn0nninf  10548  0tonninf  10549  1tonninf  10550  iseqvalcbv  10568  ser0f  10643  0exp0e1  10653  qexpcl  10664  qexpclz  10669  m1expcl2  10670  1exp  10677  sqvali  10728  sqcli  10729  sqeq0i  10730  resqcli  10733  sq1  10742  neg1sqe1  10743  iexpcyc  10753  qsqeqor  10759  facnn  10836  fac0  10837  fac1  10838  fac2  10840  fac3  10841  fac4  10842  bcval  10858  bcm1k  10869  bcpasc  10875  bccl  10876  4bc3eq4  10882  4bc2eq6  10883  hashinfom  10887  hashennn  10889  hashfz1  10892  fihasheq0  10902  hash0  10905  hashsng  10907  fihashen1  10908  omgadd  10911  hashp1i  10919  hashxp  10935  fimaxq  10936  zfz1iso  10950  wrdexi  10965  wrdv  10968  wrdeqi  10975  wrd0  10977  shftidt2  11014  cjexp  11075  re0  11077  im0  11078  re1  11079  im1  11080  cj0  11083  cji  11084  recli  11093  imcli  11094  cjcli  11095  replimi  11096  cjcji  11097  reim0bi  11098  rerebi  11099  cjrebi  11100  recji  11101  imcji  11102  cjmulrcli  11103  cjmulvali  11104  cjmulge0i  11105  renegi  11106  imnegi  11107  cjnegi  11108  addcji  11109  uzin2  11169  rexanuz  11170  rexfiuz  11171  sqrtrval  11182  sqrt0  11186  resqrexlemcalc3  11198  resqrexlemcvg  11201  resqrex  11208  abs0  11240  absi  11241  qabsor  11257  absimle  11266  recan  11291  caubnd2  11299  leabsi  11310  absrei  11311  sqrtpclii  11312  sqrtgt0ii  11313  absvalsqi  11322  absvalsq2i  11323  abscli  11324  absge0i  11325  absval2i  11326  abs00i  11327  absgt0api  11328  absnegi  11329  abscji  11330  releabsi  11331  infxrnegsupex  11445  xrbdtri  11458  cbvsum  11542  sumeq1i  11545  sum0  11570  isumz  11571  fisumss  11574  fsumsersdc  11577  fsumadd  11588  isumclim  11603  isumclim3  11605  fsumcnv  11619  modfsummodlem1  11638  fsumrelem  11653  binomlem  11665  binom  11666  arisum2  11681  expcnv  11686  0.999...  11703  prodf1f  11725  cbvprod  11740  prodeq1i  11743  zproddc  11761  zprodap0  11763  prod0  11767  fprodssdc  11772  prodsnf  11774  fprodcnv  11807  fprodge0  11819  fprodge1  11821  ef0lem  11842  esum  11844  ere  11852  ege2le3  11853  ef0  11854  eff2  11862  efsep  11873  reeff1  11882  sin0  11911  cos0  11912  ef01bndlem  11938  cos2bnd  11942  sincos1sgn  11947  sincos2sgn  11948  sin4lt0  11949  eirr  11961  0dvds  11993  dvds1  12035  z0even  12093  n2dvdsm1  12095  z2even  12096  n2dvds3  12097  ndvdssub  12112  ndvdsi  12115  flodddiv4  12118  bits0  12130  bitsfzo  12137  0bits  12141  m1bits  12142  bitsinv1lem  12143  bitsinv1  12144  gcddvds  12155  gcd1  12179  6gcd4e2  12187  bezoutlembi  12197  dfgcd3  12202  dfgcd2  12206  nninfctlemfo  12232  nninfct  12233  3lcm2e6woprm  12279  qredeu  12290  isprm2lem  12309  isprm3  12311  prm2orodd  12319  isprm5lem  12334  sqrt2irr0  12357  pw2dvds  12359  phicl2  12407  phi1  12412  dfphi2  12413  phiprmpw  12415  eulerthlemrprm  12422  eulerthlemh  12424  odzval  12435  oddprm  12453  pczpre  12491  pcdiv  12496  pc0  12498  pcqdiv  12501  pcrec  12502  pcexp  12503  pcxcl  12505  pcxqcl  12506  pcdvdstr  12521  pc2dvds  12524  dvdsprmpweqnn  12530  pcmpt  12537  qexpz  12546  pockthi  12552  1arith2  12562  4sqlemffi  12590  4sqlem11  12595  4sqlem13m  12597  4sqlem19  12603  dec2dvds  12605  dec5nprm  12608  modxai  12610  modxp1i  12612  numexp0  12616  numexp1  12617  ennnfonelemp1  12648  ennnfonelem1  12649  ennnfonelemkh  12654  ennnfonelemex  12656  ennnfonelemnn0  12664  ennnfonelemr  12665  exmidunben  12668  ctinfomlemom  12669  ctinfom  12670  ctinf  12672  qnnen  12673  omctfn  12685  omiunct  12686  ssnnctlemct  12688  nninfdc  12695  structcnvcnv  12719  structfun  12721  structfn  12722  ndxarg  12726  ndxid  12727  setsresg  12741  setsslnid  12755  basmex  12762  basmexd  12763  strleun  12807  strle1g  12809  prdsex  12971  prdsvallem  12974  prdsval  12975  prdsbaslemss  12976  imasaddfnlemg  13016  quslem  13026  xpsfrnel  13046  xpsff1o  13051  ismgmn0  13060  fn0g  13077  0g0  13078  fngsum  13090  idghm  13465  rhmfn  13804  rmodislmodlem  13982  rmodislmod  13983  lidlmex  14107  mopnset  14184  cntopex  14186  cnfldex  14191  cnfldbas  14192  mpocnfldadd  14193  mpocnfldmul  14195  cnfldcj  14197  cnfldtset  14198  cnfldle  14199  cnfldds  14200  cnring  14202  cnfld0  14203  cnfld1  14204  cnfldneg  14205  cnfldplusf  14206  cnfldsub  14207  cnfldmulg  14208  cnfldexp  14209  cnsubglem  14211  cnsubrglem  14212  gzsubrg  14214  gsumfzfsumlem0  14218  cnfldui  14221  zringring  14225  zringabl  14226  zringgrp  14227  zring1  14233  zringsubgval  14237  expghmap  14239  znval  14268  znle  14269  znbaslemnn  14271  znbas  14276  znzrh2  14278  znzrhval  14279  znzrhfo  14280  znleval  14285  znidom  14289  znidomb  14290  fnpsr  14297  psrelbas  14304  psradd  14307  psraddcl  14308  psr1clfi  14316  istopon  14333  topontopi  14336  toponunii  14337  toponrestid  14341  istps  14352  topontopn  14357  eltpsi  14361  eltg4i  14375  eltg3  14377  tg1  14379  tg2  14380  tgclb  14385  topnex  14406  sn0topon  14408  distps  14411  cldrcl  14422  sn0cld  14457  restco  14494  lmrcl  14511  ssidcn  14530  cnconst2  14553  cnptopresti  14558  cnptoprest  14559  txuni2  14576  txbas  14578  eltx  14579  txcnp  14591  upxp  14592  txcnmpt  14593  uptx  14594  txcn  14595  txrest  14596  txlm  14599  cnmptid  14601  cnmpt1st  14608  cnmpt2nd  14609  hmeofn  14622  psmetge0  14651  ismeti  14666  xmetunirn  14678  xmetge0  14685  unirnblps  14742  unirnbl  14743  mopnex  14825  qtopbasss  14841  retop  14844  uniretop  14845  iooretopg  14848  cnxmet  14851  cntoptopon  14852  cnbl0  14854  cnfldxms  14857  cnfldtps  14858  rexmet  14869  blssioo  14873  tgioo  14874  tgqioo  14875  cnopnap  14931  hovercncf  14966  limcresi  14986  dvfvalap  15001  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvcnp2cntop  15019  dvcoapbr  15027  dvexp2  15032  dvrecap  15033  dveflem  15046  dvef  15047  plyun0  15056  plyrecj  15083  dvply2  15087  reeff1o  15093  sin0pilem1  15101  sin0pilem2  15102  pilem3  15103  pigt2lt4  15104  pire  15106  sinhalfpilem  15111  pidiv2halves  15115  cosneghalfpi  15118  cospi  15120  efipi  15121  sin2pi  15123  cos2pi  15124  ef2pi  15125  cosq14gt0  15152  coseq00topi  15155  coseq0negpitopi  15156  sincos4thpi  15160  sincos6thpi  15162  sincos3rdpi  15163  pigt3  15164  cos02pilt1  15171  ioocosf1o  15174  dfrelog  15180  relogf1o  15181  relogcl  15182  relogiso  15193  rpcxpsqrt  15242  rpabscxpbnd  15260  2logb9irr  15291  2logb9irrALT  15294  sqrt2cxp2logb9e3  15295  2irrexpq  15296  2logb9irrap  15297  2irrexpqap  15298  mpodvdsmulf1o  15310  fsumdvdsmul  15311  perfectlem2  15320  lgsdir2lem1  15353  lgsdir2lem2  15354  lgsdir2lem4  15356  lgsdir2lem5  15357  lgsdi  15362  gausslemma2dlem0i  15382  gausslemma2dlem4  15389  lgseisenlem4  15398  lgsquadlem1  15402  lgsquad2lem2  15407  lgsquad2  15408  m1lgs  15410  2lgs2  15427  2lgslem4  15428  2lgsoddprmlem2  15431  2lgsoddprmlem3c  15434  2lgsoddprmlem3d  15435  2sqlem9  15449  2sqlem10  15450  ex-fl  15455  ex-ceil  15456  ex-exp  15457  ex-fac  15458  ex-gcd  15461  bj-stfal  15472  bj-stst  15475  bj-dcfal  15485  bj-dcdc  15489  bj-stdc  15490  bj-dcst  15491  bj-el2oss1o  15504  elabf2  15512  bd0  15554  bdeli  15576  bdcriota  15613  bdbm1.3ii  15621  bdinex1  15629  bdssexi  15633  bj-inex  15637  bj-snex  15643  bj-sucex  15653  bj-d0clsepcl  15655  bj-omind  15664  bj-om  15667  bj-2inf  15668  bj-peano2  15669  bdpeano5  15673  bj-omssonALT  15693  bj-inf2vnlem1  15700  bj-omex2  15707  bj-nn0sucALT  15708  012of  15724  2o01f  15725  subctctexmid  15731  nninfall  15740  nninfsellemqall  15746  nninfsellemeqinf  15747  nninfomnilem  15749  nninfomni  15750  exmidsbthrlem  15753  sbthom  15757  isomninnlem  15761  isomninn  15762  cvgcmp2nlemabs  15763  iooreen  15766  trilpolemisumle  15769  trilpolemeq1  15771  trilpo  15774  trirec0  15775  apdifflemr  15778  iswomninnlem  15780  iswomninn  15781  ismkvnnlem  15783  ismkvnn  15784  redcwlpo  15786  dcapnconst  15792  nconstwlpolem0  15794  nconstwlpo  15797  neapmkv  15799  neap0mkv  15800  taupi  15804