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

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  639  notnoti  645  pm2.21i  646  pm2.24ii  647  notbii  668  nbn  699  ori  723  orci  731  olci  732  biorfi  746  imorri  749  dcbii  840  simp1i  1006  simp2i  1007  simp3i  1008  3mix1i  1169  3mix2i  1170  3mix3i  1171  3jaoi  1303  mptru  1362  dfnot  1371  mptnan  1423  mtpor  1425  mtpxor  1426  mpg  1451  19.23h  1498  hbequid  1513  axi12  1514  nfri  1519  spi  1536  19.21  1583  eximii  1602  19.35i  1625  nfn  1658  19.37aiv  1675  19.23  1678  exan  1693  equid  1701  hbae  1718  equvini  1758  equveli  1759  sbid  1774  sbieh  1790  exdistrfor  1800  dveeq2or  1816  ax11v  1827  ax11ev  1828  equs5or  1830  sb4or  1833  sb4bor  1835  nfsb2or  1837  sbequilem  1838  sbequi  1839  speiv  1862  nfsbxy  1942  nfsbxyt  1943  sbco  1968  sbcocom  1970  sbcomxyyz  1972  sbal1yz  2001  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  eumoi  2059  moani  2096  elsb1  2155  elsb2  2156  eqeq1i  2185  eqeq2i  2188  eleq1i  2243  eleq2i  2244  nfcrii  2312  neeq1i  2362  neeq2i  2363  necon3i  2395  rspec  2529  rgen2a  2531  mprg  2534  r19.21  2553  r19.23  2585  raleqi  2677  rexeqi  2678  rabeqif  2729  elv  2742  elexi  2750  ceqsal  2767  vtocl3  2794  vtoclef  2811  vtocle  2812  spcv  2832  spcev  2833  clel3  2873  elabf  2881  elab2  2886  elab3  2890  euxfrdc  2924  reueq  2937  rmoimi2  2941  sbsbc  2967  sbc8g  2971  sbc6  2989  sbcie  2998  sbcrex  3043  csbvarg  3086  csbief  3102  csbie2  3107  sbnfc2  3118  sseli  3152  sselii  3153  sseq1i  3182  sseq2i  3183  difeq1i  3250  difeq2i  3251  uneq1i  3286  uneq2i  3287  ineq1i  3333  ineq2i  3334  ssinss1  3365  difdif2ss  3393  n0ii  3432  ne0ii  3433  vn0  3434  vn0m  3435  abf  3467  disj2  3479  difid  3492  0dif  3495  disjdif  3496  difin0  3497  undif1ss  3498  difdifdirss  3508  rgenm  3526  iftruei  3541  iffalsei  3544  ifbieq2i  3558  ifbieq12i  3560  pweqi  3580  pwid  3591  sneqi  3605  elsn  3609  elpr  3614  elsn2  3627  ralsn  3636  rexsn  3637  eltp  3641  rabrsndc  3661  preq1i  3673  preq2i  3674  prid1  3699  snnz  3712  snm  3713  prnz  3715  prm  3716  tpnz  3718  snss  3728  snsssn  3762  opeq1i  3782  opeq2i  3783  unieqi  3820  unissi  3833  inteqi  3849  intmin2  3871  intab  3874  intsn  3880  iinconstm  3896  iuniin  3897  iinss1  3899  iunxdif2  3936  ssiinf  3937  iinss  3939  iinss2  3940  iinab  3949  iundif2ss  3953  iindif2m  3955  iinin2m  3956  iunxsn  3964  iunxprg  3968  iinpw  3978  sndisj  4000  disjxsn  4002  breqi  4010  breq1i  4011  breq2i  4012  brab1  4051  opabbii  4071  truni  4116  bm1.3ii  4125  a9evsep  4126  ax9vsep  4127  zfnuleu  4128  axnul  4129  ssexi  4142  rabex  4148  elpw2  4158  pwnss  4160  iin0r  4170  intv  4171  pwex  4184  snex  4186  notnotsnex  4188  ord3ex  4191  dtruarb  4192  undifexmid  4194  intid  4225  opnzi  4236  copsexg  4245  opelopabf  4275  epelc  4292  elon  4375  inton  4394  onn0  4401  onm  4402  elsuc  4407  elsuc2  4408  sucid  4418  iunsuc  4421  onordi  4427  ontrci  4428  onelssi  4430  eusvnf  4454  ssonunii  4489  sucex  4499  onssi  4515  onsuci  4516  ordtriexmidlem  4519  ordtriexmidlem2  4520  ordtriexmid  4521  ontriexmidim  4522  ordtri2orexmid  4523  2ordpr  4524  ontr2exmid  4525  onsucsssucexmid  4527  onsucelsucexmid  4530  regexmidlemm  4532  reg2exmid  4536  onirri  4543  ruALT  4551  onprc  4552  sucon  4553  dtru  4560  0elsucexmid  4565  ordpwsucexmid  4570  ordtri2or2exmid  4571  ontri2orexmidim  4572  dcextest  4581  omex  4593  find  4599  omelon  4609  nnoni  4611  limom  4614  nnregexmid  4621  omsinds  4622  xpeq1i  4647  xpeq2i  4648  0nelxp  4655  opthprc  4678  mosubop  4693  releqi  4710  relssi  4718  relin1  4745  relin2  4746  reldif  4747  inopab  4760  difopab  4761  xpiindim  4765  opabbi2dv  4777  ideq  4780  coeq1i  4787  coeq2i  4788  cnveqi  4803  eldm  4825  eldm2  4826  dmeqi  4829  dmv  4844  rneqi  4856  elrnmpti  4881  dmex  4894  rnex  4895  reseq1i  4904  reseq2i  4905  residm  4940  resex  4949  resmpt3  4957  imaeq1i  4968  imaeq2i  4969  elima  4976  imaex  4984  elimasn  4996  args  4998  epini  5000  dfse2  5002  eliniseg2  5009  relbrcnv  5010  cotr  5011  issref  5012  cnvsym  5013  asymref  5015  intirr  5016  codir  5018  qfto  5019  ssrnres  5072  cnveq0  5086  cnvsn0  5098  dmsnop  5103  rnsnop  5110  resdm2  5120  dfco2a  5130  cocnvcnv1  5140  coi2  5146  coires1  5147  cnvssrndm  5151  cossxp  5152  cocnvres  5154  relrelss  5156  relcoi2  5160  unidmrn  5162  dfdm2  5164  unixpm  5165  cnvexg  5167  cnvex  5168  cnviinm  5171  iotaval  5190  funeqi  5238  funi  5249  funres  5258  funcnvsn  5262  funcnvcnv  5276  funin  5288  funcnvres  5290  isarep2  5304  fneq1i  5311  fneq2i  5312  fnresdisj  5327  fnresi  5334  mpt0  5344  dmmpti  5346  feq1i  5359  feq2i  5360  fdmi  5374  fun2  5390  fssres  5392  resasplitss  5396  fintm  5402  fconst6  5416  f1ores  5477  foimacnv  5480  resdif  5484  funcocnv2  5487  f1ovi  5501  fveq1i  5517  fveq2i  5519  0fv  5551  fvun1  5583  fvopab3ig  5591  fvmptss2  5592  mptrcl  5599  elfvmptrab1  5611  fndmdif  5622  fneqeql2  5626  f1oresrab  5682  fmptco  5683  fnressn  5703  fressnfv  5704  fmptap  5707  fvsnun1  5714  fvsnun2  5715  fsnunfv  5718  fconst2  5734  mptex  5743  riotabiia  5848  acexmidlema  5866  acexmidlemb  5867  acexmidlemcase  5870  acexmidlem2  5872  acexmidlemv  5873  oveq1i  5885  oveq2i  5886  oveqi  5888  oprabidlem  5906  0neqopab  5920  oprabbii  5930  oprabss  5961  mpompt  5967  funoprab  5975  fnoprab  5978  fovcl  5980  ovigg  5995  elmpocl  6069  resfunexgALT  6109  cofunexg  6110  mptexw  6114  opabex3d  6122  opabex3  6123  1st0  6145  2nd0  6146  op1st  6147  op2nd  6148  f1stres  6160  f2ndres  6161  fo1stresm  6162  fo2ndresm  6163  1stcof  6164  2ndcof  6165  1stexg  6168  2ndexg  6169  releldm2  6186  reldm  6187  dfoprab3  6192  mpomptsx  6198  mpompts  6199  fnmpoi  6205  dmmpo  6206  mpoexxg  6211  mpoexw  6214  1stconst  6222  2ndconst  6223  dfmpo  6224  algrflem  6230  algrflemg  6231  cnvoprab  6235  f1od2  6236  mpoxopn0yelv  6240  mpoxopoveq  6241  tposssxp  6250  brtpos2  6252  reldmtpos  6254  dftpos2  6262  dftpos4  6264  tpostpos  6265  tpostpos2  6266  tposfo  6272  tposf  6273  tposeqi  6278  tposex  6279  tposoprab  6281  issmo  6289  smores  6293  smores2  6295  iordsmo  6298  smo0  6299  tfrlem8  6319  tfrexlem  6335  tfr1onlem3  6339  tfr1onlemsucaccv  6342  tfr1onlembxssdm  6344  tfr1onlemres  6350  tfri1dALT  6352  tfri2  6367  rdgisuc1  6385  rdg0  6388  frecfun  6396  frec0g  6398  freccllem  6403  frecfcllem  6405  frecsuclem  6407  frecrdg  6409  2on0  6427  xp01disj  6434  2oconcl  6440  fnoa  6448  oaexg  6449  fnom  6451  omexg  6452  fnoei  6453  oeiexg  6454  oei0  6460  oacl  6461  oasuc  6465  o1p1e2  6469  omsuc  6473  nna0r  6479  nnm0r  6480  1onn  6521  2onn  6522  3onn  6523  4onn  6524  2ssom  6525  eqerlem  6566  elqs  6586  qsex  6592  ecqs  6597  iinerm  6607  th3qlem1  6637  th3q  6640  mapsn  6690  mapsnf1o3  6697  ixpiinm  6724  ixpssmap  6732  brdom  6750  f1dom  6760  enref  6765  dom2  6775  idssen  6777  ssdomg  6778  ensymi  6782  ensn1  6796  fiprc  6815  1domsn  6819  xpcomf1o  6825  xpcomco  6826  dom0  6838  0dom  6839  xpmapenlem  6849  phplem2  6853  php5  6858  snnen2og  6859  1nen2  6861  php5dom  6863  ssfilem  6875  ssfiexmid  6876  domfiexmid  6878  0fin  6884  diffitest  6887  findcard  6888  findcard2  6889  findcard2s  6890  isinfinf  6897  ac6sfi  6898  inffiexmid  6906  pw1fin  6910  unfiexmid  6917  xpfi  6929  fisseneq  6931  ssfirab  6933  en1eqsn  6947  snexxph  6949  sbthlem2  6957  sbthlemi3  6958  sbthlemi6  6961  sbthlem7  6962  fi0  6974  supeq1i  6987  infeq1i  7012  djuexb  7043  djuf1olemr  7053  inresflem  7059  djuinr  7062  updjudhcoinlf  7079  updjudhcoinrg  7080  casefun  7084  caserel  7086  caseinj  7088  caseinl  7090  caseinr  7091  omp1eomlem  7093  endjusym  7095  difinfsn  7099  difinfinf  7100  djuinj  7105  0ct  7106  ctmlemr  7107  ctssdclemn0  7109  ctssdccl  7110  omct  7116  ctfoex  7117  finomni  7138  exmidomni  7140  fodjuomni  7147  ctssexmid  7148  fodjumkv  7158  nninfwlporlem  7171  nninfwlpoimlemg  7173  nninfwlpoim  7176  card0  7187  exmidonfinlem  7192  dju1p1e2  7196  exmidfodomrlemim  7200  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  3nelsucpw1  7233  sucpw1nss3  7234  3nsssucpw1  7235  2onetap  7254  exmidmotap  7260  0npi  7312  dmaddpi  7324  dmmulpi  7325  1lt2pi  7339  0nnq  7363  1nq  7365  dmaddpq  7378  dmmulpq  7379  rec1nq  7394  1lt2nq  7405  halfnqq  7409  prarloclemarch2  7418  enq0enq  7430  nqnq0pi  7437  nnnq0lem1  7445  addnnnq0  7448  mulnnnq0  7449  nq0m0r  7455  addpinq1  7463  prarloclem5  7499  prarloclemcalc  7501  1pr  7553  1idprl  7589  1idpru  7590  ltexprlemm  7599  recexprlem1ssl  7632  recexprlem1ssu  7633  suplocexprlemell  7712  suplocexprlem2b  7713  suplocexprlemmu  7717  suplocexprlemdisj  7719  suplocexprlemloc  7720  suplocexprlemub  7722  suplocexprlemlub  7723  prsrlem1  7741  addsrpr  7744  mulsrpr  7745  gt0srpr  7747  0nsr  7748  0r  7749  1sr  7750  m1r  7751  m1m1sr  7760  caucvgsr  7801  suplocsrlempr  7806  addresr  7836  mulresr  7837  pitonnlem1  7844  peano1nnnn  7851  axi2m1  7874  axcnre  7880  peano5nnnn  7891  axcaucvg  7899  mulid1i  7959  mullidi  7960  pnfnre  7999  mnfnre  8000  pnfnemnf  8012  mnfxr  8014  rexri  8015  ltnri  8050  ltleii  8060  00id  8098  addid1i  8099  addid2i  8100  0cnALT  8147  negeqi  8151  negicn  8158  neg0  8203  renegcli  8219  negcli  8225  negidi  8226  negnegi  8227  subidi  8228  subid1i  8229  negne0bi  8230  negrebi  8231  mul02i  8347  mul01i  8348  mulm1i  8360  leidi  8442  gt0ne0ii  8444  inelr  8541  msqge0i  8574  gt0ap0ii  8585  1div1e1  8661  div1i  8697  eqnegi  8698  recclapi  8699  recidapi  8700  divmulapi  8723  rerecclapi  8734  redivclapi  8736  rerecapb  8800  recgt0  8807  ltp1i  8862  divgt0ii  8876  ltmul1ii  8885  ltdiv1ii  8886  sup3exmid  8914  peano5nni  8922  nnrei  8928  1nn  8930  nngt0i  8949  neg1ap0  9028  2timesi  9049  times2i  9050  2nn  9080  3nn  9081  4nn  9082  5nn  9083  6nn  9084  7nn  9085  8nn  9086  9nn  9087  2muline0  9144  rehalfcli  9167  nn0ssre  9180  nnnn0i  9184  dfn2  9189  0nn0  9191  nn0ge0i  9203  zrei  9259  neg1z  9285  nn0negzi  9288  dfz2  9325  nneoi  9357  peano5uzi  9362  dfuzi  9363  nn0ind-raph  9370  deceq1i  9390  deceq2i  9391  10nn  9399  numltc  9409  eluzel2  9533  eluz1i  9535  nn0uz  9562  nnuz  9563  infrenegsupex  9594  lbzbi  9616  divfnzn  9621  qdivcl  9643  irrmul  9647  cnref1o  9650  0ltpnf  9782  mnflt0  9784  0lepnf  9790  xrltnsym  9793  xrlttri3  9797  nltpnft  9814  ngtmnft  9817  xrrebnd  9819  xnegmnf  9829  xneg0  9831  xltnegi  9835  xaddmnf1  9848  xaddmnf2  9849  mnfaddpnf  9851  xaddid1  9862  xnn0lenn0nn0  9865  xnn0xadd0  9867  xposdif  9882  ixxex  9899  iooval2  9915  unirnioo  9973  ioorebasg  9975  elrege0  9976  fzval2  10011  fzen  10043  fzprval  10082  fztpval  10083  uzdisj  10093  ige2m1fz  10110  fz01or  10111  fz1ssfz0  10117  fz0sn  10121  fz0tp  10122  fz0to3un2pr  10123  fz0to4untppr  10124  nn0disj  10138  1fv  10139  4fvwrd4  10140  fzo0ss1  10174  fzo01  10216  fzo12sn  10217  fzo0to2pr  10218  fzo0to3tp  10219  fzo0to42pr  10220  qbtwnxr  10258  flval  10272  modqfrac  10337  modqmulnn  10342  q2txmodxeq0  10384  frecuzrdgdom  10418  frecuzrdgfun  10420  frecuzrdgsuct  10424  frechashgf1o  10428  nnct  10435  fxnn0nninf  10438  0tonninf  10439  1tonninf  10440  iseqvalcbv  10457  ser0f  10515  0exp0e1  10525  qexpcl  10536  qexpclz  10541  m1expcl2  10542  1exp  10549  sqvali  10600  sqcli  10601  sqeq0i  10602  resqcli  10605  sq1  10614  neg1sqe1  10615  iexpcyc  10625  qsqeqor  10631  facnn  10707  fac0  10708  fac1  10709  fac2  10711  fac3  10712  fac4  10713  bcval  10729  bcm1k  10740  bcpasc  10746  bccl  10747  4bc3eq4  10753  4bc2eq6  10754  hashinfom  10758  hashennn  10760  hashfz1  10763  fihasheq0  10773  hash0  10776  hashsng  10778  fihashen1  10779  omgadd  10782  hashp1i  10790  hashxp  10806  fimaxq  10807  zfz1iso  10821  shftidt2  10841  cjexp  10902  re0  10904  im0  10905  re1  10906  im1  10907  cj0  10910  cji  10911  recli  10920  imcli  10921  cjcli  10922  replimi  10923  cjcji  10924  reim0bi  10925  rerebi  10926  cjrebi  10927  recji  10928  imcji  10929  cjmulrcli  10930  cjmulvali  10931  cjmulge0i  10932  renegi  10933  imnegi  10934  cjnegi  10935  addcji  10936  uzin2  10996  rexanuz  10997  rexfiuz  10998  sqrtrval  11009  sqrt0  11013  resqrexlemcalc3  11025  resqrexlemcvg  11028  resqrex  11035  abs0  11067  absi  11068  qabsor  11084  absimle  11093  recan  11118  caubnd2  11126  leabsi  11137  absrei  11138  sqrtpclii  11139  sqrtgt0ii  11140  absvalsqi  11149  absvalsq2i  11150  abscli  11151  absge0i  11152  absval2i  11153  abs00i  11154  absgt0api  11155  absnegi  11156  abscji  11157  releabsi  11158  infxrnegsupex  11271  xrbdtri  11284  cbvsum  11368  sumeq1i  11371  sum0  11396  isumz  11397  fisumss  11400  fsumsersdc  11403  fsumadd  11414  isumclim  11429  isumclim3  11431  fsumcnv  11445  modfsummodlem1  11464  fsumrelem  11479  binomlem  11491  binom  11492  arisum2  11507  expcnv  11512  0.999...  11529  prodf1f  11551  cbvprod  11566  prodeq1i  11569  zproddc  11587  zprodap0  11589  prod0  11593  fprodssdc  11598  prodsnf  11600  fprodcnv  11633  fprodge0  11645  fprodge1  11647  ef0lem  11668  esum  11670  ere  11678  ege2le3  11679  ef0  11680  eff2  11688  efsep  11699  reeff1  11708  sin0  11737  cos0  11738  ef01bndlem  11764  cos2bnd  11768  sincos1sgn  11772  sincos2sgn  11773  sin4lt0  11774  eirr  11786  0dvds  11818  dvds1  11859  z0even  11916  n2dvdsm1  11918  z2even  11919  n2dvds3  11920  ndvdssub  11935  ndvdsi  11938  flodddiv4  11939  zsupssdc  11955  gcddvds  11964  gcd1  11988  6gcd4e2  11996  bezoutlembi  12006  dfgcd3  12011  dfgcd2  12015  lcmval  12063  lcmcllem  12067  lcmledvds  12070  3lcm2e6woprm  12086  qredeu  12097  isprm2lem  12116  isprm3  12118  prm2orodd  12126  isprm5lem  12141  sqrt2irr0  12164  pw2dvds  12166  phicl2  12214  phi1  12219  dfphi2  12220  phiprmpw  12222  eulerthlemrprm  12229  eulerthlemh  12231  odzval  12241  oddprm  12259  pczpre  12297  pcdiv  12302  pc0  12304  pcqdiv  12307  pcrec  12308  pcexp  12309  pcxcl  12311  pcdvdstr  12326  pc2dvds  12329  dvdsprmpweqnn  12335  pcmpt  12341  qexpz  12350  pockthi  12356  1arith2  12366  ennnfonelemp1  12407  ennnfonelem1  12408  ennnfonelemkh  12413  ennnfonelemex  12415  ennnfonelemnn0  12423  ennnfonelemr  12424  exmidunben  12427  ctinfomlemom  12428  ctinfom  12429  ctinf  12431  qnnen  12432  omctfn  12444  omiunct  12445  ssnnctlemct  12447  nninfdc  12454  structcnvcnv  12478  structfun  12480  structfn  12481  ndxarg  12485  ndxid  12486  setsresg  12500  setsslnid  12514  basmex  12521  basmexd  12522  strleun  12563  strle1g  12565  prdsex  12718  imasaddfnlemg  12735  quslem  12745  xpsfrnel  12763  xpsff1o  12768  ismgmn0  12777  fn0g  12794  0g0  12795  rmodislmodlem  13440  rmodislmod  13441  cnfldex  13461  cnfldbas  13462  cnfldadd  13463  cnfldmul  13464  cnfldcj  13465  cnring  13467  cnfld0  13468  cnfld1  13469  cnfldneg  13470  cnfldplusf  13471  cnfldsub  13472  cnfldmulg  13473  cnfldexp  13474  cnsubglem  13476  cnsubrglem  13477  gzsubrg  13479  zringring  13486  zringabl  13487  zringgrp  13488  zring1  13494  zringsubgval  13498  istopon  13516  topontopi  13519  toponunii  13520  toponrestid  13524  istps  13535  topontopn  13540  eltpsi  13544  eltg4i  13558  eltg3  13560  tg1  13562  tg2  13563  tgclb  13568  topnex  13589  sn0topon  13591  distps  13594  cldrcl  13605  sn0cld  13640  restco  13677  lmrcl  13694  ssidcn  13713  cnconst2  13736  cnptopresti  13741  cnptoprest  13742  txuni2  13759  txbas  13761  eltx  13762  txcnp  13774  upxp  13775  txcnmpt  13776  uptx  13777  txcn  13778  txrest  13779  txlm  13782  cnmptid  13784  cnmpt1st  13791  cnmpt2nd  13792  hmeofn  13805  psmetge0  13834  ismeti  13849  xmetunirn  13861  xmetge0  13868  unirnblps  13925  unirnbl  13926  mopnex  14008  qtopbasss  14024  retop  14027  uniretop  14028  iooretopg  14031  cnxmet  14034  cntoptopon  14035  cnbl0  14037  rexmet  14044  blssioo  14048  tgioo  14049  tgqioo  14050  cnopnap  14097  limcresi  14138  dvfvalap  14153  dvidlemap  14163  dvcnp2cntop  14166  dvcoapbr  14174  dvexp2  14179  dvrecap  14180  dveflem  14190  dvef  14191  reeff1o  14197  sin0pilem1  14205  sin0pilem2  14206  pilem3  14207  pigt2lt4  14208  pire  14210  sinhalfpilem  14215  pidiv2halves  14219  cosneghalfpi  14222  cospi  14224  efipi  14225  sin2pi  14227  cos2pi  14228  ef2pi  14229  cosq14gt0  14256  coseq00topi  14259  coseq0negpitopi  14260  sincos4thpi  14264  sincos6thpi  14266  sincos3rdpi  14267  pigt3  14268  cos02pilt1  14275  ioocosf1o  14278  dfrelog  14284  relogf1o  14285  relogcl  14286  relogiso  14297  rpcxpsqrt  14345  rpabscxpbnd  14362  2logb9irr  14392  2logb9irrALT  14395  sqrt2cxp2logb9e3  14396  2irrexpq  14397  2logb9irrap  14398  2irrexpqap  14399  lgsdir2lem1  14432  lgsdir2lem2  14433  lgsdir2lem4  14435  lgsdir2lem5  14436  lgsdi  14441  m1lgs  14455  2lgsoddprmlem2  14457  2lgsoddprmlem3c  14460  2lgsoddprmlem3d  14461  2sqlem9  14474  2sqlem10  14475  ex-fl  14480  ex-ceil  14481  ex-exp  14482  ex-fac  14483  ex-gcd  14486  bj-stfal  14497  bj-stst  14500  bj-dcfal  14510  bj-dcdc  14514  bj-stdc  14515  bj-dcst  14516  bj-el2oss1o  14529  elabf2  14537  bd0  14579  bdeli  14601  bdcriota  14638  bdbm1.3ii  14646  bdinex1  14654  bdssexi  14658  bj-inex  14662  bj-snex  14668  bj-sucex  14678  bj-d0clsepcl  14680  bj-omind  14689  bj-om  14692  bj-2inf  14693  bj-peano2  14694  bdpeano5  14698  bj-omssonALT  14718  bj-inf2vnlem1  14725  bj-omex2  14732  bj-nn0sucALT  14733  012of  14748  2o01f  14749  subctctexmid  14753  nninfall  14761  nninfsellemqall  14767  nninfsellemeqinf  14768  nninfomnilem  14770  nninfomni  14771  exmidsbthrlem  14773  sbthom  14777  isomninnlem  14781  isomninn  14782  cvgcmp2nlemabs  14783  iooreen  14786  trilpolemisumle  14789  trilpolemeq1  14791  trilpo  14794  trirec0  14795  apdifflemr  14798  iswomninnlem  14800  iswomninn  14801  ismkvnnlem  14803  ismkvnn  14804  redcwlpo  14806  dcapnconst  14811  nconstwlpolem0  14813  nconstwlpo  14816  neapmkv  14818  neap0mkv  14819  taupi  14823