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  mpg  1462  19.23h  1509  hbequid  1524  axi12  1525  nfri  1530  spi  1547  19.21  1594  eximii  1613  19.35i  1636  nfn  1669  19.37aiv  1686  19.23  1689  exan  1704  equid  1712  hbae  1729  equvini  1769  equveli  1770  sbid  1785  sbieh  1801  exdistrfor  1811  dveeq2or  1827  ax11v  1838  ax11ev  1839  equs5or  1841  sb4or  1844  sb4bor  1846  nfsb2or  1848  sbequilem  1849  sbequi  1850  speiv  1873  nfsbxy  1958  nfsbxyt  1959  sbco  1984  sbcocom  1986  sbcomxyyz  1988  sbal1yz  2017  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  eumoi  2075  moani  2112  elsb1  2171  elsb2  2172  eqeq1i  2201  eqeq2i  2204  eleq1i  2259  eleq2i  2260  nfcrii  2329  neeq1i  2379  neeq2i  2380  necon3i  2412  rspec  2546  rgen2a  2548  mprg  2551  r19.21  2570  r19.23  2602  raleqi  2694  rexeqi  2695  rabeqif  2751  elv  2764  elexi  2772  ceqsal  2789  vtocl3  2816  vtoclef  2833  vtocle  2834  spcv  2854  spcev  2855  clel3  2895  elabf  2903  elab2  2908  elab3  2912  euxfrdc  2946  reueq  2959  rmoimi2  2963  sbsbc  2989  sbc8g  2993  sbc6  3011  sbcie  3020  sbcrex  3065  csbvarg  3108  csbief  3125  csbie2  3130  sbnfc2  3141  sseli  3175  sselii  3176  sseq1i  3205  sseq2i  3206  difeq1i  3273  difeq2i  3274  uneq1i  3309  uneq2i  3310  ineq1i  3356  ineq2i  3357  ssinss1  3388  difdif2ss  3416  n0ii  3455  ne0ii  3456  vn0  3457  vn0m  3458  abf  3490  disj2  3502  difid  3515  0dif  3518  disjdif  3519  difin0  3520  undif1ss  3521  difdifdirss  3531  iftruei  3563  iffalsei  3566  ifbieq2i  3580  ifbieq12i  3582  pweqi  3605  pwid  3616  sneqi  3630  elsn  3634  elpr  3639  elsn2  3652  ralsn  3661  rexsn  3662  eltp  3666  rabrsndc  3686  preq1i  3698  preq2i  3699  prid1  3724  snnz  3737  snm  3738  prnz  3740  prm  3741  tpnz  3743  snss  3753  snsssn  3787  opeq1i  3807  opeq2i  3808  unieqi  3845  unissi  3858  inteqi  3874  intmin2  3896  intab  3899  intsn  3905  iinconstm  3921  iuniin  3922  iinss1  3924  iunxdif2  3961  ssiinf  3962  iinss  3964  iinss2  3965  iinab  3974  iundif2ss  3978  iindif2m  3980  iinin2m  3981  iunxsn  3989  iunxprg  3993  iinpw  4003  sndisj  4025  disjxsn  4027  breqi  4035  breq1i  4036  breq2i  4037  brab1  4076  opabbii  4096  truni  4141  bm1.3ii  4150  a9evsep  4151  ax9vsep  4152  zfnuleu  4153  axnul  4154  ssexi  4167  rabex  4173  rabex2  4175  elpw2  4186  pwnss  4188  iin0r  4198  intv  4199  pwex  4212  snex  4214  notnotsnex  4216  ord3ex  4219  dtruarb  4220  undifexmid  4222  intid  4253  opnzi  4264  copsexg  4273  opelopabf  4305  epelc  4322  elon  4405  inton  4424  onn0  4431  onm  4432  elsuc  4437  elsuc2  4438  sucid  4448  iunsuc  4451  onordi  4457  ontrci  4458  onelssi  4460  eusvnf  4484  ssonunii  4521  sucex  4531  onssi  4547  onsuci  4548  ordtriexmidlem  4551  ordtriexmidlem2  4552  ordtriexmid  4553  ontriexmidim  4554  ordtri2orexmid  4555  2ordpr  4556  ontr2exmid  4557  onsucsssucexmid  4559  onsucelsucexmid  4562  regexmidlemm  4564  reg2exmid  4568  onirri  4575  ruALT  4583  onprc  4584  sucon  4585  dtru  4592  0elsucexmid  4597  ordpwsucexmid  4602  ordtri2or2exmid  4603  ontri2orexmidim  4604  dcextest  4613  omex  4625  find  4631  omelon  4641  nnoni  4643  limom  4646  nnregexmid  4653  omsinds  4654  xpeq1i  4679  xpeq2i  4680  0nelxp  4687  opthprc  4710  mosubop  4725  releqi  4742  relssi  4750  relin1  4777  relin2  4778  reldif  4779  inopab  4794  difopab  4795  xpiindim  4799  opabbi2dv  4811  ideq  4814  coeq1i  4821  coeq2i  4822  cnveqi  4837  eldm  4859  eldm2  4860  dmeqi  4863  dmv  4878  rneqi  4890  elrnmpti  4915  dmex  4928  rnex  4929  reseq1i  4938  reseq2i  4939  residm  4974  resex  4983  resmpt3  4991  imaeq1i  5002  imaeq2i  5003  elima  5010  imaex  5020  elimasn  5032  args  5034  epini  5036  dfse2  5038  eliniseg2  5045  relbrcnv  5046  cotr  5047  issref  5048  cnvsym  5049  asymref  5051  intirr  5052  codir  5054  qfto  5055  ssrnres  5108  cnveq0  5122  cnvsn0  5134  dmsnop  5139  rnsnop  5146  resdm2  5156  dfco2a  5166  cocnvcnv1  5176  coi2  5182  coires1  5183  cnvssrndm  5187  cossxp  5188  cocnvres  5190  relrelss  5192  relcoi2  5196  unidmrn  5198  dfdm2  5200  unixpm  5201  cnvexg  5203  cnvex  5204  cnviinm  5207  iotaval  5226  funeqi  5275  funi  5286  funres  5295  funcnvsn  5299  funcnvcnv  5313  funin  5325  funcnvres  5327  isarep2  5341  fneq1i  5348  fneq2i  5349  fnresdisj  5364  fnresi  5371  mpt0  5381  dmmpti  5383  feq1i  5396  feq2i  5397  fdmi  5411  fun2  5427  fssres  5429  resasplitss  5433  fintm  5439  fconst6  5453  f1ores  5515  foimacnv  5518  resdif  5522  funcocnv2  5525  f1ovi  5539  fveq1i  5555  fveq2i  5557  0fv  5590  fvun1  5623  fvopab3ig  5631  fvmptss2  5632  mptrcl  5640  elfvmptrab1  5652  fndmdif  5663  fneqeql2  5667  f1oresrab  5723  fmptco  5724  fnressn  5744  fressnfv  5745  fmptap  5748  fvsnun1  5755  fvsnun2  5756  fsnunfv  5759  fconst2  5775  mptex  5784  riotabiia  5891  acexmidlema  5909  acexmidlemb  5910  acexmidlemcase  5913  acexmidlem2  5915  acexmidlemv  5916  oveq1i  5928  oveq2i  5929  oveqi  5931  oprabidlem  5949  0neqopab  5963  oprabbii  5973  oprabss  6004  mpompt  6010  funoprab  6018  fnoprab  6021  ovigg  6039  elmpocl  6113  resfunexgALT  6160  cofunexg  6161  mptexw  6165  opabex3d  6173  opabex3  6174  1st0  6197  2nd0  6198  op1st  6199  op2nd  6200  f1stres  6212  f2ndres  6213  fo1stresm  6214  fo2ndresm  6215  1stcof  6216  2ndcof  6217  1stexg  6220  2ndexg  6221  releldm2  6238  reldm  6239  dfoprab3  6244  mpomptsx  6250  mpompts  6251  fnmpoi  6257  dmmpo  6258  mpoexxg  6263  mpoexw  6266  1stconst  6274  2ndconst  6275  dfmpo  6276  algrflem  6282  algrflemg  6283  cnvoprab  6287  f1od2  6288  mpoxopn0yelv  6292  mpoxopoveq  6293  tposssxp  6302  brtpos2  6304  reldmtpos  6306  dftpos2  6314  dftpos4  6316  tpostpos  6317  tpostpos2  6318  tposfo  6324  tposf  6325  tposeqi  6330  tposex  6331  tposoprab  6333  issmo  6341  smores  6345  smores2  6347  iordsmo  6350  smo0  6351  tfrlem8  6371  tfrexlem  6387  tfr1onlem3  6391  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlemres  6402  tfri1dALT  6404  tfri2  6419  rdgisuc1  6437  rdg0  6440  frecfun  6448  frec0g  6450  freccllem  6455  frecfcllem  6457  frecsuclem  6459  frecrdg  6461  2on0  6479  xp01disj  6486  2oconcl  6492  fnoa  6500  oaexg  6501  fnom  6503  omexg  6504  fnoei  6505  oeiexg  6506  oei0  6512  oacl  6513  oasuc  6517  o1p1e2  6521  omsuc  6525  nna0r  6531  nnm0r  6532  1onn  6573  2onn  6574  3onn  6575  4onn  6576  2ssom  6577  eqerlem  6618  eceq2i  6625  elqs  6640  qsex  6646  ecqs  6651  iinerm  6661  th3qlem1  6691  th3q  6694  mapsn  6744  mapsnf1o3  6751  ixpiinm  6778  ixpssmap  6786  brdom  6804  f1dom  6814  enref  6819  dom2  6829  idssen  6831  ssdomg  6832  ensymi  6836  ensn1  6850  fiprc  6869  1domsn  6873  xpcomf1o  6879  xpcomco  6880  dom0  6894  0dom  6895  xpmapenlem  6905  phplem2  6909  php5  6914  snnen2og  6915  1nen2  6917  php5dom  6919  ssfilem  6931  ssfiexmid  6932  domfiexmid  6934  0fin  6940  diffitest  6943  findcard  6944  findcard2  6945  findcard2s  6946  isinfinf  6953  ac6sfi  6954  inffiexmid  6962  pw1fin  6966  unfiexmid  6974  xpfi  6986  fisseneq  6988  ssfirab  6990  residfi  6999  en1eqsn  7007  snexxph  7009  sbthlem2  7017  sbthlemi3  7018  sbthlemi6  7021  sbthlem7  7022  fi0  7034  supeq1i  7047  infeq1i  7072  djuexb  7103  djuf1olemr  7113  inresflem  7119  djuinr  7122  updjudhcoinlf  7139  updjudhcoinrg  7140  casefun  7144  caserel  7146  caseinj  7148  caseinl  7150  caseinr  7151  omp1eomlem  7153  endjusym  7155  difinfsn  7159  difinfinf  7160  djuinj  7165  0ct  7166  ctmlemr  7167  ctssdclemn0  7169  ctssdccl  7170  omct  7176  ctfoex  7177  finomni  7199  exmidomni  7201  fodjuomni  7208  ctssexmid  7209  fodjumkv  7219  nninfwlporlem  7232  nninfwlpoimlemg  7234  nninfwlpoim  7237  card0  7248  exmidonfinlem  7253  dju1p1e2  7257  exmidfodomrlemim  7261  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  3nelsucpw1  7294  sucpw1nss3  7295  3nsssucpw1  7296  2onetap  7315  exmidmotap  7321  0npi  7373  dmaddpi  7385  dmmulpi  7386  1lt2pi  7400  0nnq  7424  1nq  7426  dmaddpq  7439  dmmulpq  7440  rec1nq  7455  1lt2nq  7466  halfnqq  7470  prarloclemarch2  7479  enq0enq  7491  nqnq0pi  7498  nnnq0lem1  7506  addnnnq0  7509  mulnnnq0  7510  nq0m0r  7516  addpinq1  7524  prarloclem5  7560  prarloclemcalc  7562  1pr  7614  1idprl  7650  1idpru  7651  ltexprlemm  7660  recexprlem1ssl  7693  recexprlem1ssu  7694  suplocexprlemell  7773  suplocexprlem2b  7774  suplocexprlemmu  7778  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemub  7783  suplocexprlemlub  7784  prsrlem1  7802  addsrpr  7805  mulsrpr  7806  gt0srpr  7808  0nsr  7809  0r  7810  1sr  7811  m1r  7812  m1m1sr  7821  caucvgsr  7862  suplocsrlempr  7867  addresr  7897  mulresr  7898  pitonnlem1  7905  peano1nnnn  7912  axi2m1  7935  axcnre  7941  peano5nnnn  7952  axcaucvg  7960  mpomulf  8009  mulid1i  8021  mullidi  8022  pnfnre  8061  mnfnre  8062  pnfnemnf  8074  mnfxr  8076  rexri  8077  ltnri  8112  ltleii  8122  00id  8160  addid1i  8161  addid2i  8162  0cnALT  8209  negeqi  8213  negicn  8220  neg0  8265  renegcli  8281  negcli  8287  negidi  8288  negnegi  8289  subidi  8290  subid1i  8291  negne0bi  8292  negrebi  8293  mul02i  8409  mul01i  8410  mulm1i  8422  leidi  8504  gt0ne0ii  8506  inelr  8603  msqge0i  8636  gt0ap0ii  8647  1div1e1  8723  div1i  8759  eqnegi  8760  recclapi  8761  recidapi  8762  divmulapi  8785  rerecclapi  8796  redivclapi  8798  rerecapb  8862  recgt0  8869  ltp1i  8924  divgt0ii  8938  ltmul1ii  8947  ltdiv1ii  8948  sup3exmid  8976  peano5nni  8985  nnrei  8991  1nn  8993  nngt0i  9012  neg1ap0  9091  2timesi  9112  times2i  9113  2nn  9143  3nn  9144  4nn  9145  5nn  9146  6nn  9147  7nn  9148  8nn  9149  9nn  9150  2muline0  9207  rehalfcli  9231  nn0ssre  9244  nnnn0i  9248  dfn2  9253  0nn0  9255  nn0ge0i  9267  zrei  9323  neg1z  9349  nn0negzi  9352  dfz2  9389  nneoi  9421  peano5uzi  9426  dfuzi  9427  nn0ind-raph  9434  deceq1i  9454  deceq2i  9455  10nn  9463  numltc  9473  eluzel2  9597  eluz1i  9599  nn0uz  9627  nnuz  9628  infrenegsupex  9659  lbzbi  9681  divfnzn  9686  qdivcl  9708  irrmul  9712  irrmulap  9713  cnref1o  9716  0ltpnf  9848  mnflt0  9850  0lepnf  9856  xrltnsym  9859  xrlttri3  9863  nltpnft  9880  ngtmnft  9883  xrrebnd  9885  xnegmnf  9895  xneg0  9897  xltnegi  9901  xaddmnf1  9914  xaddmnf2  9915  mnfaddpnf  9917  xaddid1  9928  xnn0lenn0nn0  9931  xnn0xadd0  9933  xposdif  9948  ixxex  9965  iooval2  9981  unirnioo  10039  ioorebasg  10041  elrege0  10042  fzval2  10077  fzen  10109  fzprval  10148  fztpval  10149  uzdisj  10159  ige2m1fz  10176  fz01or  10177  fz1ssfz0  10183  fz0sn  10187  fz0tp  10188  fz0to3un2pr  10189  fz0to4untppr  10190  nn0disj  10204  1fv  10205  4fvwrd4  10206  fzo0ss1  10241  fzo01  10283  fzo12sn  10284  fzo0to2pr  10285  fzo0to3tp  10286  fzo0to42pr  10287  qbtwnxr  10326  flval  10341  fldiv4lem1div2  10376  modqfrac  10408  modqmulnn  10413  q2txmodxeq0  10455  frecuzrdgdom  10489  frecuzrdgfun  10491  frecuzrdgsuct  10495  frechashgf1o  10499  nnct  10506  xnn0nnen  10508  fxnn0nninf  10510  0tonninf  10511  1tonninf  10512  iseqvalcbv  10530  ser0f  10605  0exp0e1  10615  qexpcl  10626  qexpclz  10631  m1expcl2  10632  1exp  10639  sqvali  10690  sqcli  10691  sqeq0i  10692  resqcli  10695  sq1  10704  neg1sqe1  10705  iexpcyc  10715  qsqeqor  10721  facnn  10798  fac0  10799  fac1  10800  fac2  10802  fac3  10803  fac4  10804  bcval  10820  bcm1k  10831  bcpasc  10837  bccl  10838  4bc3eq4  10844  4bc2eq6  10845  hashinfom  10849  hashennn  10851  hashfz1  10854  fihasheq0  10864  hash0  10867  hashsng  10869  fihashen1  10870  omgadd  10873  hashp1i  10881  hashxp  10897  fimaxq  10898  zfz1iso  10912  wrdexi  10927  wrdv  10930  wrdeqi  10937  wrd0  10939  shftidt2  10976  cjexp  11037  re0  11039  im0  11040  re1  11041  im1  11042  cj0  11045  cji  11046  recli  11055  imcli  11056  cjcli  11057  replimi  11058  cjcji  11059  reim0bi  11060  rerebi  11061  cjrebi  11062  recji  11063  imcji  11064  cjmulrcli  11065  cjmulvali  11066  cjmulge0i  11067  renegi  11068  imnegi  11069  cjnegi  11070  addcji  11071  uzin2  11131  rexanuz  11132  rexfiuz  11133  sqrtrval  11144  sqrt0  11148  resqrexlemcalc3  11160  resqrexlemcvg  11163  resqrex  11170  abs0  11202  absi  11203  qabsor  11219  absimle  11228  recan  11253  caubnd2  11261  leabsi  11272  absrei  11273  sqrtpclii  11274  sqrtgt0ii  11275  absvalsqi  11284  absvalsq2i  11285  abscli  11286  absge0i  11287  absval2i  11288  abs00i  11289  absgt0api  11290  absnegi  11291  abscji  11292  releabsi  11293  infxrnegsupex  11406  xrbdtri  11419  cbvsum  11503  sumeq1i  11506  sum0  11531  isumz  11532  fisumss  11535  fsumsersdc  11538  fsumadd  11549  isumclim  11564  isumclim3  11566  fsumcnv  11580  modfsummodlem1  11599  fsumrelem  11614  binomlem  11626  binom  11627  arisum2  11642  expcnv  11647  0.999...  11664  prodf1f  11686  cbvprod  11701  prodeq1i  11704  zproddc  11722  zprodap0  11724  prod0  11728  fprodssdc  11733  prodsnf  11735  fprodcnv  11768  fprodge0  11780  fprodge1  11782  ef0lem  11803  esum  11805  ere  11813  ege2le3  11814  ef0  11815  eff2  11823  efsep  11834  reeff1  11843  sin0  11872  cos0  11873  ef01bndlem  11899  cos2bnd  11903  sincos1sgn  11908  sincos2sgn  11909  sin4lt0  11910  eirr  11922  0dvds  11954  dvds1  11995  z0even  12052  n2dvdsm1  12054  z2even  12055  n2dvds3  12056  ndvdssub  12071  ndvdsi  12074  flodddiv4  12075  zsupssdc  12091  gcddvds  12100  gcd1  12124  6gcd4e2  12132  bezoutlembi  12142  dfgcd3  12147  dfgcd2  12151  nninfctlemfo  12177  nninfct  12178  3lcm2e6woprm  12224  qredeu  12235  isprm2lem  12254  isprm3  12256  prm2orodd  12264  isprm5lem  12279  sqrt2irr0  12302  pw2dvds  12304  phicl2  12352  phi1  12357  dfphi2  12358  phiprmpw  12360  eulerthlemrprm  12367  eulerthlemh  12369  odzval  12379  oddprm  12397  pczpre  12435  pcdiv  12440  pc0  12442  pcqdiv  12445  pcrec  12446  pcexp  12447  pcxcl  12449  pcxqcl  12450  pcdvdstr  12465  pc2dvds  12468  dvdsprmpweqnn  12474  pcmpt  12481  qexpz  12490  pockthi  12496  1arith2  12506  4sqlemffi  12534  4sqlem11  12539  4sqlem13m  12541  4sqlem19  12547  ennnfonelemp1  12563  ennnfonelem1  12564  ennnfonelemkh  12569  ennnfonelemex  12571  ennnfonelemnn0  12579  ennnfonelemr  12580  exmidunben  12583  ctinfomlemom  12584  ctinfom  12585  ctinf  12587  qnnen  12588  omctfn  12600  omiunct  12601  ssnnctlemct  12603  nninfdc  12610  structcnvcnv  12634  structfun  12636  structfn  12637  ndxarg  12641  ndxid  12642  setsresg  12656  setsslnid  12670  basmex  12677  basmexd  12678  strleun  12722  strle1g  12724  prdsex  12880  imasaddfnlemg  12897  quslem  12907  xpsfrnel  12927  xpsff1o  12932  ismgmn0  12941  fn0g  12958  0g0  12959  fngsum  12971  idghm  13329  rhmfn  13668  rmodislmodlem  13846  rmodislmod  13847  lidlmex  13971  cnfldex  14050  cnfldbas  14051  cnfldadd  14052  cnfldmul  14054  cnfldcj  14056  cnring  14058  cnfld0  14059  cnfld1  14060  cnfldneg  14061  cnfldplusf  14062  cnfldsub  14063  cnfldmulg  14064  cnfldexp  14065  cnsubglem  14067  cnsubrglem  14068  gzsubrg  14070  gsumfzfsumlem0  14074  cnfldui  14077  zringring  14081  zringabl  14082  zringgrp  14083  zring1  14089  zringsubgval  14093  expghmap  14095  znval  14124  znle  14125  znbaslemnn  14127  znbas  14132  znzrh2  14134  znzrhval  14135  znzrhfo  14136  znleval  14141  znidom  14145  znidomb  14146  fnpsr  14153  psrelbas  14160  psradd  14163  psraddcl  14164  istopon  14181  topontopi  14184  toponunii  14185  toponrestid  14189  istps  14200  topontopn  14205  eltpsi  14209  eltg4i  14223  eltg3  14225  tg1  14227  tg2  14228  tgclb  14233  topnex  14254  sn0topon  14256  distps  14259  cldrcl  14270  sn0cld  14305  restco  14342  lmrcl  14359  ssidcn  14378  cnconst2  14401  cnptopresti  14406  cnptoprest  14407  txuni2  14424  txbas  14426  eltx  14427  txcnp  14439  upxp  14440  txcnmpt  14441  uptx  14442  txcn  14443  txrest  14444  txlm  14447  cnmptid  14449  cnmpt1st  14456  cnmpt2nd  14457  hmeofn  14470  psmetge0  14499  ismeti  14514  xmetunirn  14526  xmetge0  14533  unirnblps  14590  unirnbl  14591  mopnex  14673  qtopbasss  14689  retop  14692  uniretop  14693  iooretopg  14696  cnxmet  14699  cntoptopon  14700  cnbl0  14702  rexmet  14709  blssioo  14713  tgioo  14714  tgqioo  14715  cnopnap  14765  hovercncf  14800  limcresi  14820  dvfvalap  14835  dvidlemap  14845  dvcnp2cntop  14848  dvcoapbr  14856  dvexp2  14861  dvrecap  14862  dveflem  14872  dvef  14873  plyun0  14882  reeff1o  14908  sin0pilem1  14916  sin0pilem2  14917  pilem3  14918  pigt2lt4  14919  pire  14921  sinhalfpilem  14926  pidiv2halves  14930  cosneghalfpi  14933  cospi  14935  efipi  14936  sin2pi  14938  cos2pi  14939  ef2pi  14940  cosq14gt0  14967  coseq00topi  14970  coseq0negpitopi  14971  sincos4thpi  14975  sincos6thpi  14977  sincos3rdpi  14978  pigt3  14979  cos02pilt1  14986  ioocosf1o  14989  dfrelog  14995  relogf1o  14996  relogcl  14997  relogiso  15008  rpcxpsqrt  15056  rpabscxpbnd  15073  2logb9irr  15103  2logb9irrALT  15106  sqrt2cxp2logb9e3  15107  2irrexpq  15108  2logb9irrap  15109  2irrexpqap  15110  lgsdir2lem1  15144  lgsdir2lem2  15145  lgsdir2lem4  15147  lgsdir2lem5  15148  lgsdi  15153  gausslemma2dlem0i  15173  gausslemma2dlem4  15180  lgseisenlem4  15189  lgsquadlem1  15191  m1lgs  15192  2lgsoddprmlem2  15194  2lgsoddprmlem3c  15197  2lgsoddprmlem3d  15198  2sqlem9  15211  2sqlem10  15212  ex-fl  15217  ex-ceil  15218  ex-exp  15219  ex-fac  15220  ex-gcd  15223  bj-stfal  15234  bj-stst  15237  bj-dcfal  15247  bj-dcdc  15251  bj-stdc  15252  bj-dcst  15253  bj-el2oss1o  15266  elabf2  15274  bd0  15316  bdeli  15338  bdcriota  15375  bdbm1.3ii  15383  bdinex1  15391  bdssexi  15395  bj-inex  15399  bj-snex  15405  bj-sucex  15415  bj-d0clsepcl  15417  bj-omind  15426  bj-om  15429  bj-2inf  15430  bj-peano2  15431  bdpeano5  15435  bj-omssonALT  15455  bj-inf2vnlem1  15462  bj-omex2  15469  bj-nn0sucALT  15470  012of  15486  2o01f  15487  subctctexmid  15491  nninfall  15499  nninfsellemqall  15505  nninfsellemeqinf  15506  nninfomnilem  15508  nninfomni  15509  exmidsbthrlem  15512  sbthom  15516  isomninnlem  15520  isomninn  15521  cvgcmp2nlemabs  15522  iooreen  15525  trilpolemisumle  15528  trilpolemeq1  15530  trilpo  15533  trirec0  15534  apdifflemr  15537  iswomninnlem  15539  iswomninn  15540  ismkvnnlem  15542  ismkvnn  15543  redcwlpo  15545  dcapnconst  15551  nconstwlpolem0  15553  nconstwlpo  15556  neapmkv  15558  neap0mkv  15559  taupi  15563