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  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  1954  nfsbxyt  1955  sbco  1980  sbcocom  1982  sbcomxyyz  1984  sbal1yz  2013  dvelimALT  2022  dvelimfv  2023  dvelimor  2030  eumoi  2071  moani  2108  elsb1  2167  elsb2  2168  eqeq1i  2197  eqeq2i  2200  eleq1i  2255  eleq2i  2256  nfcrii  2325  neeq1i  2375  neeq2i  2376  necon3i  2408  rspec  2542  rgen2a  2544  mprg  2547  r19.21  2566  r19.23  2598  raleqi  2690  rexeqi  2691  rabeqif  2747  elv  2760  elexi  2768  ceqsal  2785  vtocl3  2812  vtoclef  2829  vtocle  2830  spcv  2850  spcev  2851  clel3  2891  elabf  2899  elab2  2904  elab3  2908  euxfrdc  2942  reueq  2955  rmoimi2  2959  sbsbc  2985  sbc8g  2989  sbc6  3007  sbcie  3016  sbcrex  3061  csbvarg  3104  csbief  3121  csbie2  3126  sbnfc2  3137  sseli  3171  sselii  3172  sseq1i  3201  sseq2i  3202  difeq1i  3269  difeq2i  3270  uneq1i  3305  uneq2i  3306  ineq1i  3352  ineq2i  3353  ssinss1  3384  difdif2ss  3412  n0ii  3451  ne0ii  3452  vn0  3453  vn0m  3454  abf  3486  disj2  3498  difid  3511  0dif  3514  disjdif  3515  difin0  3516  undif1ss  3517  difdifdirss  3527  iftruei  3559  iffalsei  3562  ifbieq2i  3576  ifbieq12i  3578  pweqi  3601  pwid  3612  sneqi  3626  elsn  3630  elpr  3635  elsn2  3648  ralsn  3657  rexsn  3658  eltp  3662  rabrsndc  3682  preq1i  3694  preq2i  3695  prid1  3720  snnz  3733  snm  3734  prnz  3736  prm  3737  tpnz  3739  snss  3749  snsssn  3783  opeq1i  3803  opeq2i  3804  unieqi  3841  unissi  3854  inteqi  3870  intmin2  3892  intab  3895  intsn  3901  iinconstm  3917  iuniin  3918  iinss1  3920  iunxdif2  3957  ssiinf  3958  iinss  3960  iinss2  3961  iinab  3970  iundif2ss  3974  iindif2m  3976  iinin2m  3977  iunxsn  3985  iunxprg  3989  iinpw  3999  sndisj  4021  disjxsn  4023  breqi  4031  breq1i  4032  breq2i  4033  brab1  4072  opabbii  4092  truni  4137  bm1.3ii  4146  a9evsep  4147  ax9vsep  4148  zfnuleu  4149  axnul  4150  ssexi  4163  rabex  4169  rabex2  4171  elpw2  4182  pwnss  4184  iin0r  4194  intv  4195  pwex  4208  snex  4210  notnotsnex  4212  ord3ex  4215  dtruarb  4216  undifexmid  4218  intid  4249  opnzi  4260  copsexg  4269  opelopabf  4299  epelc  4316  elon  4399  inton  4418  onn0  4425  onm  4426  elsuc  4431  elsuc2  4432  sucid  4442  iunsuc  4445  onordi  4451  ontrci  4452  onelssi  4454  eusvnf  4478  ssonunii  4513  sucex  4523  onssi  4539  onsuci  4540  ordtriexmidlem  4543  ordtriexmidlem2  4544  ordtriexmid  4545  ontriexmidim  4546  ordtri2orexmid  4547  2ordpr  4548  ontr2exmid  4549  onsucsssucexmid  4551  onsucelsucexmid  4554  regexmidlemm  4556  reg2exmid  4560  onirri  4567  ruALT  4575  onprc  4576  sucon  4577  dtru  4584  0elsucexmid  4589  ordpwsucexmid  4594  ordtri2or2exmid  4595  ontri2orexmidim  4596  dcextest  4605  omex  4617  find  4623  omelon  4633  nnoni  4635  limom  4638  nnregexmid  4645  omsinds  4646  xpeq1i  4671  xpeq2i  4672  0nelxp  4679  opthprc  4702  mosubop  4717  releqi  4734  relssi  4742  relin1  4769  relin2  4770  reldif  4771  inopab  4784  difopab  4785  xpiindim  4789  opabbi2dv  4801  ideq  4804  coeq1i  4811  coeq2i  4812  cnveqi  4827  eldm  4849  eldm2  4850  dmeqi  4853  dmv  4868  rneqi  4880  elrnmpti  4905  dmex  4918  rnex  4919  reseq1i  4928  reseq2i  4929  residm  4964  resex  4973  resmpt3  4981  imaeq1i  4992  imaeq2i  4993  elima  5000  imaex  5008  elimasn  5020  args  5022  epini  5024  dfse2  5026  eliniseg2  5033  relbrcnv  5034  cotr  5035  issref  5036  cnvsym  5037  asymref  5039  intirr  5040  codir  5042  qfto  5043  ssrnres  5096  cnveq0  5110  cnvsn0  5122  dmsnop  5127  rnsnop  5134  resdm2  5144  dfco2a  5154  cocnvcnv1  5164  coi2  5170  coires1  5171  cnvssrndm  5175  cossxp  5176  cocnvres  5178  relrelss  5180  relcoi2  5184  unidmrn  5186  dfdm2  5188  unixpm  5189  cnvexg  5191  cnvex  5192  cnviinm  5195  iotaval  5214  funeqi  5263  funi  5274  funres  5283  funcnvsn  5287  funcnvcnv  5301  funin  5313  funcnvres  5315  isarep2  5329  fneq1i  5336  fneq2i  5337  fnresdisj  5352  fnresi  5359  mpt0  5369  dmmpti  5371  feq1i  5384  feq2i  5385  fdmi  5399  fun2  5415  fssres  5417  resasplitss  5421  fintm  5427  fconst6  5441  f1ores  5503  foimacnv  5506  resdif  5510  funcocnv2  5513  f1ovi  5527  fveq1i  5543  fveq2i  5545  0fv  5578  fvun1  5611  fvopab3ig  5619  fvmptss2  5620  mptrcl  5628  elfvmptrab1  5640  fndmdif  5651  fneqeql2  5655  f1oresrab  5711  fmptco  5712  fnressn  5732  fressnfv  5733  fmptap  5736  fvsnun1  5743  fvsnun2  5744  fsnunfv  5747  fconst2  5763  mptex  5772  riotabiia  5879  acexmidlema  5897  acexmidlemb  5898  acexmidlemcase  5901  acexmidlem2  5903  acexmidlemv  5904  oveq1i  5916  oveq2i  5917  oveqi  5919  oprabidlem  5937  0neqopab  5951  oprabbii  5961  oprabss  5992  mpompt  5998  funoprab  6006  fnoprab  6009  ovigg  6027  elmpocl  6101  resfunexgALT  6148  cofunexg  6149  mptexw  6153  opabex3d  6161  opabex3  6162  1st0  6184  2nd0  6185  op1st  6186  op2nd  6187  f1stres  6199  f2ndres  6200  fo1stresm  6201  fo2ndresm  6202  1stcof  6203  2ndcof  6204  1stexg  6207  2ndexg  6208  releldm2  6225  reldm  6226  dfoprab3  6231  mpomptsx  6237  mpompts  6238  fnmpoi  6244  dmmpo  6245  mpoexxg  6250  mpoexw  6253  1stconst  6261  2ndconst  6262  dfmpo  6263  algrflem  6269  algrflemg  6270  cnvoprab  6274  f1od2  6275  mpoxopn0yelv  6279  mpoxopoveq  6280  tposssxp  6289  brtpos2  6291  reldmtpos  6293  dftpos2  6301  dftpos4  6303  tpostpos  6304  tpostpos2  6305  tposfo  6311  tposf  6312  tposeqi  6317  tposex  6318  tposoprab  6320  issmo  6328  smores  6332  smores2  6334  iordsmo  6337  smo0  6338  tfrlem8  6358  tfrexlem  6374  tfr1onlem3  6378  tfr1onlemsucaccv  6381  tfr1onlembxssdm  6383  tfr1onlemres  6389  tfri1dALT  6391  tfri2  6406  rdgisuc1  6424  rdg0  6427  frecfun  6435  frec0g  6437  freccllem  6442  frecfcllem  6444  frecsuclem  6446  frecrdg  6448  2on0  6466  xp01disj  6473  2oconcl  6479  fnoa  6487  oaexg  6488  fnom  6490  omexg  6491  fnoei  6492  oeiexg  6493  oei0  6499  oacl  6500  oasuc  6504  o1p1e2  6508  omsuc  6512  nna0r  6518  nnm0r  6519  1onn  6560  2onn  6561  3onn  6562  4onn  6563  2ssom  6564  eqerlem  6605  eceq2i  6612  elqs  6627  qsex  6633  ecqs  6638  iinerm  6648  th3qlem1  6678  th3q  6681  mapsn  6731  mapsnf1o3  6738  ixpiinm  6765  ixpssmap  6773  brdom  6791  f1dom  6801  enref  6806  dom2  6816  idssen  6818  ssdomg  6819  ensymi  6823  ensn1  6837  fiprc  6856  1domsn  6860  xpcomf1o  6866  xpcomco  6867  dom0  6881  0dom  6882  xpmapenlem  6892  phplem2  6896  php5  6901  snnen2og  6902  1nen2  6904  php5dom  6906  ssfilem  6918  ssfiexmid  6919  domfiexmid  6921  0fin  6927  diffitest  6930  findcard  6931  findcard2  6932  findcard2s  6933  isinfinf  6940  ac6sfi  6941  inffiexmid  6949  pw1fin  6953  unfiexmid  6961  xpfi  6973  fisseneq  6975  ssfirab  6977  residfi  6985  en1eqsn  6993  snexxph  6995  sbthlem2  7003  sbthlemi3  7004  sbthlemi6  7007  sbthlem7  7008  fi0  7020  supeq1i  7033  infeq1i  7058  djuexb  7089  djuf1olemr  7099  inresflem  7105  djuinr  7108  updjudhcoinlf  7125  updjudhcoinrg  7126  casefun  7130  caserel  7132  caseinj  7134  caseinl  7136  caseinr  7137  omp1eomlem  7139  endjusym  7141  difinfsn  7145  difinfinf  7146  djuinj  7151  0ct  7152  ctmlemr  7153  ctssdclemn0  7155  ctssdccl  7156  omct  7162  ctfoex  7163  finomni  7185  exmidomni  7187  fodjuomni  7194  ctssexmid  7195  fodjumkv  7205  nninfwlporlem  7218  nninfwlpoimlemg  7220  nninfwlpoim  7223  card0  7234  exmidonfinlem  7239  dju1p1e2  7243  exmidfodomrlemim  7247  exmidfodomrlemr  7248  exmidfodomrlemrALT  7249  3nelsucpw1  7280  sucpw1nss3  7281  3nsssucpw1  7282  2onetap  7301  exmidmotap  7307  0npi  7359  dmaddpi  7371  dmmulpi  7372  1lt2pi  7386  0nnq  7410  1nq  7412  dmaddpq  7425  dmmulpq  7426  rec1nq  7441  1lt2nq  7452  halfnqq  7456  prarloclemarch2  7465  enq0enq  7477  nqnq0pi  7484  nnnq0lem1  7492  addnnnq0  7495  mulnnnq0  7496  nq0m0r  7502  addpinq1  7510  prarloclem5  7546  prarloclemcalc  7548  1pr  7600  1idprl  7636  1idpru  7637  ltexprlemm  7646  recexprlem1ssl  7679  recexprlem1ssu  7680  suplocexprlemell  7759  suplocexprlem2b  7760  suplocexprlemmu  7764  suplocexprlemdisj  7766  suplocexprlemloc  7767  suplocexprlemub  7769  suplocexprlemlub  7770  prsrlem1  7788  addsrpr  7791  mulsrpr  7792  gt0srpr  7794  0nsr  7795  0r  7796  1sr  7797  m1r  7798  m1m1sr  7807  caucvgsr  7848  suplocsrlempr  7853  addresr  7883  mulresr  7884  pitonnlem1  7891  peano1nnnn  7898  axi2m1  7921  axcnre  7927  peano5nnnn  7938  axcaucvg  7946  mpomulf  7995  mulid1i  8007  mullidi  8008  pnfnre  8047  mnfnre  8048  pnfnemnf  8060  mnfxr  8062  rexri  8063  ltnri  8098  ltleii  8108  00id  8146  addid1i  8147  addid2i  8148  0cnALT  8195  negeqi  8199  negicn  8206  neg0  8251  renegcli  8267  negcli  8273  negidi  8274  negnegi  8275  subidi  8276  subid1i  8277  negne0bi  8278  negrebi  8279  mul02i  8395  mul01i  8396  mulm1i  8408  leidi  8490  gt0ne0ii  8492  inelr  8589  msqge0i  8622  gt0ap0ii  8633  1div1e1  8709  div1i  8745  eqnegi  8746  recclapi  8747  recidapi  8748  divmulapi  8771  rerecclapi  8782  redivclapi  8784  rerecapb  8848  recgt0  8855  ltp1i  8910  divgt0ii  8924  ltmul1ii  8933  ltdiv1ii  8934  sup3exmid  8962  peano5nni  8971  nnrei  8977  1nn  8979  nngt0i  8998  neg1ap0  9077  2timesi  9098  times2i  9099  2nn  9129  3nn  9130  4nn  9131  5nn  9132  6nn  9133  7nn  9134  8nn  9135  9nn  9136  2muline0  9193  rehalfcli  9217  nn0ssre  9230  nnnn0i  9234  dfn2  9239  0nn0  9241  nn0ge0i  9253  zrei  9309  neg1z  9335  nn0negzi  9338  dfz2  9375  nneoi  9407  peano5uzi  9412  dfuzi  9413  nn0ind-raph  9420  deceq1i  9440  deceq2i  9441  10nn  9449  numltc  9459  eluzel2  9583  eluz1i  9585  nn0uz  9613  nnuz  9614  infrenegsupex  9645  lbzbi  9667  divfnzn  9672  qdivcl  9694  irrmul  9698  irrmulap  9699  cnref1o  9702  0ltpnf  9834  mnflt0  9836  0lepnf  9842  xrltnsym  9845  xrlttri3  9849  nltpnft  9866  ngtmnft  9869  xrrebnd  9871  xnegmnf  9881  xneg0  9883  xltnegi  9887  xaddmnf1  9900  xaddmnf2  9901  mnfaddpnf  9903  xaddid1  9914  xnn0lenn0nn0  9917  xnn0xadd0  9919  xposdif  9934  ixxex  9951  iooval2  9967  unirnioo  10025  ioorebasg  10027  elrege0  10028  fzval2  10063  fzen  10095  fzprval  10134  fztpval  10135  uzdisj  10145  ige2m1fz  10162  fz01or  10163  fz1ssfz0  10169  fz0sn  10173  fz0tp  10174  fz0to3un2pr  10175  fz0to4untppr  10176  nn0disj  10190  1fv  10191  4fvwrd4  10192  fzo0ss1  10227  fzo01  10269  fzo12sn  10270  fzo0to2pr  10271  fzo0to3tp  10272  fzo0to42pr  10273  qbtwnxr  10312  flval  10327  fldiv4lem1div2  10362  modqfrac  10394  modqmulnn  10399  q2txmodxeq0  10441  frecuzrdgdom  10475  frecuzrdgfun  10477  frecuzrdgsuct  10481  frechashgf1o  10485  nnct  10492  xnn0nnen  10494  fxnn0nninf  10496  0tonninf  10497  1tonninf  10498  iseqvalcbv  10516  ser0f  10579  0exp0e1  10589  qexpcl  10600  qexpclz  10605  m1expcl2  10606  1exp  10613  sqvali  10664  sqcli  10665  sqeq0i  10666  resqcli  10669  sq1  10678  neg1sqe1  10679  iexpcyc  10689  qsqeqor  10695  facnn  10772  fac0  10773  fac1  10774  fac2  10776  fac3  10777  fac4  10778  bcval  10794  bcm1k  10805  bcpasc  10811  bccl  10812  4bc3eq4  10818  4bc2eq6  10819  hashinfom  10823  hashennn  10825  hashfz1  10828  fihasheq0  10838  hash0  10841  hashsng  10843  fihashen1  10844  omgadd  10847  hashp1i  10855  hashxp  10871  fimaxq  10872  zfz1iso  10886  wrdexi  10901  wrdv  10904  wrdeqi  10911  wrd0  10913  shftidt2  10950  cjexp  11011  re0  11013  im0  11014  re1  11015  im1  11016  cj0  11019  cji  11020  recli  11029  imcli  11030  cjcli  11031  replimi  11032  cjcji  11033  reim0bi  11034  rerebi  11035  cjrebi  11036  recji  11037  imcji  11038  cjmulrcli  11039  cjmulvali  11040  cjmulge0i  11041  renegi  11042  imnegi  11043  cjnegi  11044  addcji  11045  uzin2  11105  rexanuz  11106  rexfiuz  11107  sqrtrval  11118  sqrt0  11122  resqrexlemcalc3  11134  resqrexlemcvg  11137  resqrex  11144  abs0  11176  absi  11177  qabsor  11193  absimle  11202  recan  11227  caubnd2  11235  leabsi  11246  absrei  11247  sqrtpclii  11248  sqrtgt0ii  11249  absvalsqi  11258  absvalsq2i  11259  abscli  11260  absge0i  11261  absval2i  11262  abs00i  11263  absgt0api  11264  absnegi  11265  abscji  11266  releabsi  11267  infxrnegsupex  11380  xrbdtri  11393  cbvsum  11477  sumeq1i  11480  sum0  11505  isumz  11506  fisumss  11509  fsumsersdc  11512  fsumadd  11523  isumclim  11538  isumclim3  11540  fsumcnv  11554  modfsummodlem1  11573  fsumrelem  11588  binomlem  11600  binom  11601  arisum2  11616  expcnv  11621  0.999...  11638  prodf1f  11660  cbvprod  11675  prodeq1i  11678  zproddc  11696  zprodap0  11698  prod0  11702  fprodssdc  11707  prodsnf  11709  fprodcnv  11742  fprodge0  11754  fprodge1  11756  ef0lem  11777  esum  11779  ere  11787  ege2le3  11788  ef0  11789  eff2  11797  efsep  11808  reeff1  11817  sin0  11846  cos0  11847  ef01bndlem  11873  cos2bnd  11877  sincos1sgn  11882  sincos2sgn  11883  sin4lt0  11884  eirr  11896  0dvds  11928  dvds1  11969  z0even  12026  n2dvdsm1  12028  z2even  12029  n2dvds3  12030  ndvdssub  12045  ndvdsi  12048  flodddiv4  12049  zsupssdc  12065  gcddvds  12074  gcd1  12098  6gcd4e2  12106  bezoutlembi  12116  dfgcd3  12121  dfgcd2  12125  nninfctlemfo  12151  nninfct  12152  3lcm2e6woprm  12198  qredeu  12209  isprm2lem  12228  isprm3  12230  prm2orodd  12238  isprm5lem  12253  sqrt2irr0  12276  pw2dvds  12278  phicl2  12326  phi1  12331  dfphi2  12332  phiprmpw  12334  eulerthlemrprm  12341  eulerthlemh  12343  odzval  12353  oddprm  12371  pczpre  12409  pcdiv  12414  pc0  12416  pcqdiv  12419  pcrec  12420  pcexp  12421  pcxcl  12423  pcxqcl  12424  pcdvdstr  12439  pc2dvds  12442  dvdsprmpweqnn  12448  pcmpt  12455  qexpz  12464  pockthi  12470  1arith2  12480  4sqlemffi  12508  4sqlem11  12513  4sqlem13m  12515  4sqlem19  12521  ennnfonelemp1  12537  ennnfonelem1  12538  ennnfonelemkh  12543  ennnfonelemex  12545  ennnfonelemnn0  12553  ennnfonelemr  12554  exmidunben  12557  ctinfomlemom  12558  ctinfom  12559  ctinf  12561  qnnen  12562  omctfn  12574  omiunct  12575  ssnnctlemct  12577  nninfdc  12584  structcnvcnv  12608  structfun  12610  structfn  12611  ndxarg  12615  ndxid  12616  setsresg  12630  setsslnid  12644  basmex  12651  basmexd  12652  strleun  12696  strle1g  12698  prdsex  12854  imasaddfnlemg  12871  quslem  12881  xpsfrnel  12901  xpsff1o  12906  ismgmn0  12915  fn0g  12932  0g0  12933  fngsum  12945  idghm  13302  rhmfn  13632  rmodislmodlem  13810  rmodislmod  13811  lidlmex  13935  cnfldex  14014  cnfldbas  14015  cnfldadd  14016  cnfldmul  14017  cnfldcj  14018  cnring  14020  cnfld0  14021  cnfld1  14022  cnfldneg  14023  cnfldplusf  14024  cnfldsub  14025  cnfldmulg  14026  cnfldexp  14027  cnsubglem  14029  cnsubrglem  14030  gzsubrg  14032  zringring  14039  zringabl  14040  zringgrp  14041  zring1  14047  zringsubgval  14051  znval  14081  znle  14082  znbaslemnn  14084  znbas  14089  znzrh2  14091  znzrhval  14092  znzrhfo  14093  znleval  14098  znidom  14102  znidomb  14103  fnpsr  14110  psrelbas  14117  psradd  14120  psraddcl  14121  istopon  14138  topontopi  14141  toponunii  14142  toponrestid  14146  istps  14157  topontopn  14162  eltpsi  14166  eltg4i  14180  eltg3  14182  tg1  14184  tg2  14185  tgclb  14190  topnex  14211  sn0topon  14213  distps  14216  cldrcl  14227  sn0cld  14262  restco  14299  lmrcl  14316  ssidcn  14335  cnconst2  14358  cnptopresti  14363  cnptoprest  14364  txuni2  14381  txbas  14383  eltx  14384  txcnp  14396  upxp  14397  txcnmpt  14398  uptx  14399  txcn  14400  txrest  14401  txlm  14404  cnmptid  14406  cnmpt1st  14413  cnmpt2nd  14414  hmeofn  14427  psmetge0  14456  ismeti  14471  xmetunirn  14483  xmetge0  14490  unirnblps  14547  unirnbl  14548  mopnex  14630  qtopbasss  14646  retop  14649  uniretop  14650  iooretopg  14653  cnxmet  14656  cntoptopon  14657  cnbl0  14659  rexmet  14666  blssioo  14670  tgioo  14671  tgqioo  14672  cnopnap  14722  hovercncf  14757  limcresi  14777  dvfvalap  14792  dvidlemap  14802  dvcnp2cntop  14805  dvcoapbr  14813  dvexp2  14818  dvrecap  14819  dveflem  14829  dvef  14830  reeff1o  14836  sin0pilem1  14844  sin0pilem2  14845  pilem3  14846  pigt2lt4  14847  pire  14849  sinhalfpilem  14854  pidiv2halves  14858  cosneghalfpi  14861  cospi  14863  efipi  14864  sin2pi  14866  cos2pi  14867  ef2pi  14868  cosq14gt0  14895  coseq00topi  14898  coseq0negpitopi  14899  sincos4thpi  14903  sincos6thpi  14905  sincos3rdpi  14906  pigt3  14907  cos02pilt1  14914  ioocosf1o  14917  dfrelog  14923  relogf1o  14924  relogcl  14925  relogiso  14936  rpcxpsqrt  14984  rpabscxpbnd  15001  2logb9irr  15031  2logb9irrALT  15034  sqrt2cxp2logb9e3  15035  2irrexpq  15036  2logb9irrap  15037  2irrexpqap  15038  lgsdir2lem1  15072  lgsdir2lem2  15073  lgsdir2lem4  15075  lgsdir2lem5  15076  lgsdi  15081  gausslemma2dlem0i  15101  gausslemma2dlem4  15108  m1lgs  15116  2lgsoddprmlem2  15118  2lgsoddprmlem3c  15121  2lgsoddprmlem3d  15122  2sqlem9  15135  2sqlem10  15136  ex-fl  15141  ex-ceil  15142  ex-exp  15143  ex-fac  15144  ex-gcd  15147  bj-stfal  15158  bj-stst  15161  bj-dcfal  15171  bj-dcdc  15175  bj-stdc  15176  bj-dcst  15177  bj-el2oss1o  15190  elabf2  15198  bd0  15240  bdeli  15262  bdcriota  15299  bdbm1.3ii  15307  bdinex1  15315  bdssexi  15319  bj-inex  15323  bj-snex  15329  bj-sucex  15339  bj-d0clsepcl  15341  bj-omind  15350  bj-om  15353  bj-2inf  15354  bj-peano2  15355  bdpeano5  15359  bj-omssonALT  15379  bj-inf2vnlem1  15386  bj-omex2  15393  bj-nn0sucALT  15394  012of  15410  2o01f  15411  subctctexmid  15415  nninfall  15423  nninfsellemqall  15429  nninfsellemeqinf  15430  nninfomnilem  15432  nninfomni  15433  exmidsbthrlem  15436  sbthom  15440  isomninnlem  15444  isomninn  15445  cvgcmp2nlemabs  15446  iooreen  15449  trilpolemisumle  15452  trilpolemeq1  15454  trilpo  15457  trirec0  15458  apdifflemr  15461  iswomninnlem  15463  iswomninn  15464  ismkvnnlem  15466  ismkvnn  15467  redcwlpo  15469  dcapnconst  15475  nconstwlpolem0  15477  nconstwlpo  15480  neapmkv  15482  neap0mkv  15483  taupi  15487