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  7254  nninfinfwlpo  7255  card0  7268  ficardon  7269  exmidonfinlem  7274  dju1p1e2  7278  exmidfodomrlemim  7282  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  3nelsucpw1  7319  sucpw1nss3  7320  3nsssucpw1  7321  2onetap  7340  exmidmotap  7346  0npi  7399  dmaddpi  7411  dmmulpi  7412  1lt2pi  7426  0nnq  7450  1nq  7452  dmaddpq  7465  dmmulpq  7466  rec1nq  7481  1lt2nq  7492  halfnqq  7496  prarloclemarch2  7505  enq0enq  7517  nqnq0pi  7524  nnnq0lem1  7532  addnnnq0  7535  mulnnnq0  7536  nq0m0r  7542  addpinq1  7550  prarloclem5  7586  prarloclemcalc  7588  1pr  7640  1idprl  7676  1idpru  7677  ltexprlemm  7686  recexprlem1ssl  7719  recexprlem1ssu  7720  suplocexprlemell  7799  suplocexprlem2b  7800  suplocexprlemmu  7804  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemub  7809  suplocexprlemlub  7810  prsrlem1  7828  addsrpr  7831  mulsrpr  7832  gt0srpr  7834  0nsr  7835  0r  7836  1sr  7837  m1r  7838  m1m1sr  7847  caucvgsr  7888  suplocsrlempr  7893  addresr  7923  mulresr  7924  pitonnlem1  7931  peano1nnnn  7938  axi2m1  7961  axcnre  7967  peano5nnnn  7978  axcaucvg  7986  mpomulf  8035  mulridi  8047  mullidi  8048  pnfnre  8087  mnfnre  8088  pnfnemnf  8100  mnfxr  8102  rexri  8103  ltnri  8138  ltleii  8148  00id  8186  addridi  8187  addlidi  8188  0cnALT  8235  negeqi  8239  negicn  8246  neg0  8291  renegcli  8307  negcli  8313  negidi  8314  negnegi  8315  subidi  8316  subid1i  8317  negne0bi  8318  negrebi  8319  mul02i  8435  mul01i  8436  mulm1i  8448  leidi  8531  gt0ne0ii  8533  inelr  8630  msqge0i  8663  gt0ap0ii  8674  1div1e1  8750  div1i  8786  eqnegi  8787  recclapi  8788  recidapi  8789  divmulapi  8812  rerecclapi  8823  redivclapi  8825  rerecapb  8889  recgt0  8896  ltp1i  8951  divgt0ii  8965  ltmul1ii  8974  ltdiv1ii  8975  sup3exmid  9003  peano5nni  9012  nnrei  9018  1nn  9020  nngt0i  9039  neg1ap0  9118  2timesi  9139  times2i  9140  2nn  9171  3nn  9172  4nn  9173  5nn  9174  6nn  9175  7nn  9176  8nn  9177  9nn  9178  2muline0  9235  rehalfcli  9259  nn0ssre  9272  nnnn0i  9276  dfn2  9281  0nn0  9283  nn0ge0i  9295  zrei  9351  neg1z  9377  nn0negzi  9380  dfz2  9417  nneoi  9449  peano5uzi  9454  dfuzi  9455  nn0ind-raph  9462  deceq1i  9482  deceq2i  9483  10nn  9491  numltc  9501  eluzel2  9625  eluz1i  9627  nn0uz  9655  nnuz  9656  infrenegsupex  9687  lbzbi  9709  divfnzn  9714  qdivcl  9736  irrmul  9740  irrmulap  9741  cnref1o  9744  0ltpnf  9876  mnflt0  9878  0lepnf  9884  xrltnsym  9887  xrlttri3  9891  nltpnft  9908  ngtmnft  9911  xrrebnd  9913  xnegmnf  9923  xneg0  9925  xltnegi  9929  xaddmnf1  9942  xaddmnf2  9943  mnfaddpnf  9945  xaddid1  9956  xnn0lenn0nn0  9959  xnn0xadd0  9961  xposdif  9976  ixxex  9993  iooval2  10009  unirnioo  10067  ioorebasg  10069  elrege0  10070  fzval2  10105  fzen  10137  fzprval  10176  fztpval  10177  uzdisj  10187  ige2m1fz  10204  fz01or  10205  fz1ssfz0  10211  fz0sn  10215  fz0tp  10216  fz0to3un2pr  10217  fz0to4untppr  10218  nn0disj  10232  1fv  10233  4fvwrd4  10234  fzo0ss1  10269  fzo01  10311  fzo12sn  10312  fzo0to2pr  10313  fzo0to3tp  10314  fzo0to42pr  10315  zsupssdc  10347  qbtwnxr  10366  flval  10381  fldiv4lem1div2  10416  modqfrac  10448  modqmulnn  10453  q2txmodxeq0  10495  frecuzrdgdom  10529  frecuzrdgfun  10531  frecuzrdgsuct  10535  frechashgf1o  10539  nnct  10546  xnn0nnen  10548  fxnn0nninf  10550  0tonninf  10551  1tonninf  10552  iseqvalcbv  10570  ser0f  10645  0exp0e1  10655  qexpcl  10666  qexpclz  10671  m1expcl2  10672  1exp  10679  sqvali  10730  sqcli  10731  sqeq0i  10732  resqcli  10735  sq1  10744  neg1sqe1  10745  iexpcyc  10755  qsqeqor  10761  facnn  10838  fac0  10839  fac1  10840  fac2  10842  fac3  10843  fac4  10844  bcval  10860  bcm1k  10871  bcpasc  10877  bccl  10878  4bc3eq4  10884  4bc2eq6  10885  hashinfom  10889  hashennn  10891  hashfz1  10894  fihasheq0  10904  hash0  10907  hashsng  10909  fihashen1  10910  omgadd  10913  hashp1i  10921  hashxp  10937  fimaxq  10938  zfz1iso  10952  wrdexi  10967  wrdv  10970  wrdeqi  10977  wrd0  10979  shftidt2  11016  cjexp  11077  re0  11079  im0  11080  re1  11081  im1  11082  cj0  11085  cji  11086  recli  11095  imcli  11096  cjcli  11097  replimi  11098  cjcji  11099  reim0bi  11100  rerebi  11101  cjrebi  11102  recji  11103  imcji  11104  cjmulrcli  11105  cjmulvali  11106  cjmulge0i  11107  renegi  11108  imnegi  11109  cjnegi  11110  addcji  11111  uzin2  11171  rexanuz  11172  rexfiuz  11173  sqrtrval  11184  sqrt0  11188  resqrexlemcalc3  11200  resqrexlemcvg  11203  resqrex  11210  abs0  11242  absi  11243  qabsor  11259  absimle  11268  recan  11293  caubnd2  11301  leabsi  11312  absrei  11313  sqrtpclii  11314  sqrtgt0ii  11315  absvalsqi  11324  absvalsq2i  11325  abscli  11326  absge0i  11327  absval2i  11328  abs00i  11329  absgt0api  11330  absnegi  11331  abscji  11332  releabsi  11333  infxrnegsupex  11447  xrbdtri  11460  cbvsum  11544  sumeq1i  11547  sum0  11572  isumz  11573  fisumss  11576  fsumsersdc  11579  fsumadd  11590  isumclim  11605  isumclim3  11607  fsumcnv  11621  modfsummodlem1  11640  fsumrelem  11655  binomlem  11667  binom  11668  arisum2  11683  expcnv  11688  0.999...  11705  prodf1f  11727  cbvprod  11742  prodeq1i  11745  zproddc  11763  zprodap0  11765  prod0  11769  fprodssdc  11774  prodsnf  11776  fprodcnv  11809  fprodge0  11821  fprodge1  11823  ef0lem  11844  esum  11846  ere  11854  ege2le3  11855  ef0  11856  eff2  11864  efsep  11875  reeff1  11884  sin0  11913  cos0  11914  ef01bndlem  11940  cos2bnd  11944  sincos1sgn  11949  sincos2sgn  11950  sin4lt0  11951  eirr  11963  0dvds  11995  dvds1  12037  z0even  12095  n2dvdsm1  12097  z2even  12098  n2dvds3  12099  ndvdssub  12114  ndvdsi  12117  flodddiv4  12120  bits0  12132  bitsfzo  12139  0bits  12143  m1bits  12144  bitsinv1lem  12145  bitsinv1  12146  gcddvds  12157  gcd1  12181  6gcd4e2  12189  bezoutlembi  12199  dfgcd3  12204  dfgcd2  12208  nninfctlemfo  12234  nninfct  12235  3lcm2e6woprm  12281  qredeu  12292  isprm2lem  12311  isprm3  12313  prm2orodd  12321  isprm5lem  12336  sqrt2irr0  12359  pw2dvds  12361  phicl2  12409  phi1  12414  dfphi2  12415  phiprmpw  12417  eulerthlemrprm  12424  eulerthlemh  12426  odzval  12437  oddprm  12455  pczpre  12493  pcdiv  12498  pc0  12500  pcqdiv  12503  pcrec  12504  pcexp  12505  pcxcl  12507  pcxqcl  12508  pcdvdstr  12523  pc2dvds  12526  dvdsprmpweqnn  12532  pcmpt  12539  qexpz  12548  pockthi  12554  1arith2  12564  4sqlemffi  12592  4sqlem11  12597  4sqlem13m  12599  4sqlem19  12605  dec2dvds  12607  dec5nprm  12610  modxai  12612  modxp1i  12614  numexp0  12618  numexp1  12619  ennnfonelemp1  12650  ennnfonelem1  12651  ennnfonelemkh  12656  ennnfonelemex  12658  ennnfonelemnn0  12666  ennnfonelemr  12667  exmidunben  12670  ctinfomlemom  12671  ctinfom  12672  ctinf  12674  qnnen  12675  omctfn  12687  omiunct  12688  ssnnctlemct  12690  nninfdc  12697  structcnvcnv  12721  structfun  12723  structfn  12724  ndxarg  12728  ndxid  12729  setsresg  12743  setsslnid  12757  basmex  12764  basmexd  12765  strleun  12809  strle1g  12811  prdsex  12973  prdsvallem  12976  prdsval  12977  prdsbaslemss  12978  imasaddfnlemg  13018  quslem  13028  xpsfrnel  13048  xpsff1o  13053  ismgmn0  13062  fn0g  13079  0g0  13080  fngsum  13092  idghm  13467  rhmfn  13806  rmodislmodlem  13984  rmodislmod  13985  lidlmex  14109  mopnset  14186  cntopex  14188  cnfldex  14193  cnfldbas  14194  mpocnfldadd  14195  mpocnfldmul  14197  cnfldcj  14199  cnfldtset  14200  cnfldle  14201  cnfldds  14202  cnring  14204  cnfld0  14205  cnfld1  14206  cnfldneg  14207  cnfldplusf  14208  cnfldsub  14209  cnfldmulg  14210  cnfldexp  14211  cnsubglem  14213  cnsubrglem  14214  gzsubrg  14216  gsumfzfsumlem0  14220  cnfldui  14223  zringring  14227  zringabl  14228  zringgrp  14229  zring1  14235  zringsubgval  14239  expghmap  14241  znval  14270  znle  14271  znbaslemnn  14273  znbas  14278  znzrh2  14280  znzrhval  14281  znzrhfo  14282  znleval  14287  znidom  14291  znidomb  14292  fnpsr  14299  psrelbas  14306  psradd  14309  psraddcl  14310  psr1clfi  14318  istopon  14335  topontopi  14338  toponunii  14339  toponrestid  14343  istps  14354  topontopn  14359  eltpsi  14363  eltg4i  14377  eltg3  14379  tg1  14381  tg2  14382  tgclb  14387  topnex  14408  sn0topon  14410  distps  14413  cldrcl  14424  sn0cld  14459  restco  14496  lmrcl  14513  ssidcn  14532  cnconst2  14555  cnptopresti  14560  cnptoprest  14561  txuni2  14578  txbas  14580  eltx  14581  txcnp  14593  upxp  14594  txcnmpt  14595  uptx  14596  txcn  14597  txrest  14598  txlm  14601  cnmptid  14603  cnmpt1st  14610  cnmpt2nd  14611  hmeofn  14624  psmetge0  14653  ismeti  14668  xmetunirn  14680  xmetge0  14687  unirnblps  14744  unirnbl  14745  mopnex  14827  qtopbasss  14843  retop  14846  uniretop  14847  iooretopg  14850  cnxmet  14853  cntoptopon  14854  cnbl0  14856  cnfldxms  14859  cnfldtps  14860  rexmet  14871  blssioo  14875  tgioo  14876  tgqioo  14877  cnopnap  14933  hovercncf  14968  limcresi  14988  dvfvalap  15003  dvidlemap  15013  dvidrelem  15014  dvidsslem  15015  dvcnp2cntop  15021  dvcoapbr  15029  dvexp2  15034  dvrecap  15035  dveflem  15048  dvef  15049  plyun0  15058  plyrecj  15085  dvply2  15089  reeff1o  15095  sin0pilem1  15103  sin0pilem2  15104  pilem3  15105  pigt2lt4  15106  pire  15108  sinhalfpilem  15113  pidiv2halves  15117  cosneghalfpi  15120  cospi  15122  efipi  15123  sin2pi  15125  cos2pi  15126  ef2pi  15127  cosq14gt0  15154  coseq00topi  15157  coseq0negpitopi  15158  sincos4thpi  15162  sincos6thpi  15164  sincos3rdpi  15165  pigt3  15166  cos02pilt1  15173  ioocosf1o  15176  dfrelog  15182  relogf1o  15183  relogcl  15184  relogiso  15195  rpcxpsqrt  15244  rpabscxpbnd  15262  2logb9irr  15293  2logb9irrALT  15296  sqrt2cxp2logb9e3  15297  2irrexpq  15298  2logb9irrap  15299  2irrexpqap  15300  mpodvdsmulf1o  15312  fsumdvdsmul  15313  perfectlem2  15322  lgsdir2lem1  15355  lgsdir2lem2  15356  lgsdir2lem4  15358  lgsdir2lem5  15359  lgsdi  15364  gausslemma2dlem0i  15384  gausslemma2dlem4  15391  lgseisenlem4  15400  lgsquadlem1  15404  lgsquad2lem2  15409  lgsquad2  15410  m1lgs  15412  2lgs2  15429  2lgslem4  15430  2lgsoddprmlem2  15433  2lgsoddprmlem3c  15436  2lgsoddprmlem3d  15437  2sqlem9  15451  2sqlem10  15452  ex-fl  15457  ex-ceil  15458  ex-exp  15459  ex-fac  15460  ex-gcd  15463  bj-stfal  15474  bj-stst  15477  bj-dcfal  15487  bj-dcdc  15491  bj-stdc  15492  bj-dcst  15493  bj-el2oss1o  15506  elabf2  15514  bd0  15556  bdeli  15578  bdcriota  15615  bdbm1.3ii  15623  bdinex1  15631  bdssexi  15635  bj-inex  15639  bj-snex  15645  bj-sucex  15655  bj-d0clsepcl  15657  bj-omind  15666  bj-om  15669  bj-2inf  15670  bj-peano2  15671  bdpeano5  15675  bj-omssonALT  15695  bj-inf2vnlem1  15702  bj-omex2  15709  bj-nn0sucALT  15710  012of  15726  2o01f  15727  subctctexmid  15733  nninfall  15742  nninfsellemqall  15748  nninfsellemeqinf  15749  nninfomnilem  15751  nninfomni  15752  exmidsbthrlem  15757  sbthom  15761  isomninnlem  15765  isomninn  15766  cvgcmp2nlemabs  15767  iooreen  15770  trilpolemisumle  15773  trilpolemeq1  15775  trilpo  15778  trirec0  15779  apdifflemr  15782  iswomninnlem  15784  iswomninn  15785  ismkvnnlem  15787  ismkvnn  15788  redcwlpo  15790  dcapnconst  15796  nconstwlpolem0  15798  nconstwlpo  15801  neapmkv  15803  neap0mkv  15804  taupi  15808