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  1007  simp2i  1008  simp3i  1009  3mix1i  1170  3mix2i  1171  3mix3i  1172  3jaoi  1313  mptru  1372  dfnot  1381  mptnan  1433  mtpor  1435  mtpxor  1436  mpg  1461  19.23h  1508  hbequid  1523  axi12  1524  nfri  1529  spi  1546  19.21  1593  eximii  1612  19.35i  1635  nfn  1668  19.37aiv  1685  19.23  1688  exan  1703  equid  1711  hbae  1728  equvini  1768  equveli  1769  sbid  1784  sbieh  1800  exdistrfor  1810  dveeq2or  1826  ax11v  1837  ax11ev  1838  equs5or  1840  sb4or  1843  sb4bor  1845  nfsb2or  1847  sbequilem  1848  sbequi  1849  speiv  1872  nfsbxy  1952  nfsbxyt  1953  sbco  1978  sbcocom  1980  sbcomxyyz  1982  sbal1yz  2011  dvelimALT  2020  dvelimfv  2021  dvelimor  2028  eumoi  2069  moani  2106  elsb1  2165  elsb2  2166  eqeq1i  2195  eqeq2i  2198  eleq1i  2253  eleq2i  2254  nfcrii  2322  neeq1i  2372  neeq2i  2373  necon3i  2405  rspec  2539  rgen2a  2541  mprg  2544  r19.21  2563  r19.23  2595  raleqi  2687  rexeqi  2688  rabeqif  2740  elv  2753  elexi  2761  ceqsal  2778  vtocl3  2805  vtoclef  2822  vtocle  2823  spcv  2843  spcev  2844  clel3  2884  elabf  2892  elab2  2897  elab3  2901  euxfrdc  2935  reueq  2948  rmoimi2  2952  sbsbc  2978  sbc8g  2982  sbc6  3000  sbcie  3009  sbcrex  3054  csbvarg  3097  csbief  3113  csbie2  3118  sbnfc2  3129  sseli  3163  sselii  3164  sseq1i  3193  sseq2i  3194  difeq1i  3261  difeq2i  3262  uneq1i  3297  uneq2i  3298  ineq1i  3344  ineq2i  3345  ssinss1  3376  difdif2ss  3404  n0ii  3443  ne0ii  3444  vn0  3445  vn0m  3446  abf  3478  disj2  3490  difid  3503  0dif  3506  disjdif  3507  difin0  3508  undif1ss  3509  difdifdirss  3519  rgenm  3537  iftruei  3552  iffalsei  3555  ifbieq2i  3569  ifbieq12i  3571  pweqi  3591  pwid  3602  sneqi  3616  elsn  3620  elpr  3625  elsn2  3638  ralsn  3647  rexsn  3648  eltp  3652  rabrsndc  3672  preq1i  3684  preq2i  3685  prid1  3710  snnz  3723  snm  3724  prnz  3726  prm  3727  tpnz  3729  snss  3739  snsssn  3773  opeq1i  3793  opeq2i  3794  unieqi  3831  unissi  3844  inteqi  3860  intmin2  3882  intab  3885  intsn  3891  iinconstm  3907  iuniin  3908  iinss1  3910  iunxdif2  3947  ssiinf  3948  iinss  3950  iinss2  3951  iinab  3960  iundif2ss  3964  iindif2m  3966  iinin2m  3967  iunxsn  3975  iunxprg  3979  iinpw  3989  sndisj  4011  disjxsn  4013  breqi  4021  breq1i  4022  breq2i  4023  brab1  4062  opabbii  4082  truni  4127  bm1.3ii  4136  a9evsep  4137  ax9vsep  4138  zfnuleu  4139  axnul  4140  ssexi  4153  rabex  4159  elpw2  4169  pwnss  4171  iin0r  4181  intv  4182  pwex  4195  snex  4197  notnotsnex  4199  ord3ex  4202  dtruarb  4203  undifexmid  4205  intid  4236  opnzi  4247  copsexg  4256  opelopabf  4286  epelc  4303  elon  4386  inton  4405  onn0  4412  onm  4413  elsuc  4418  elsuc2  4419  sucid  4429  iunsuc  4432  onordi  4438  ontrci  4439  onelssi  4441  eusvnf  4465  ssonunii  4500  sucex  4510  onssi  4526  onsuci  4527  ordtriexmidlem  4530  ordtriexmidlem2  4531  ordtriexmid  4532  ontriexmidim  4533  ordtri2orexmid  4534  2ordpr  4535  ontr2exmid  4536  onsucsssucexmid  4538  onsucelsucexmid  4541  regexmidlemm  4543  reg2exmid  4547  onirri  4554  ruALT  4562  onprc  4563  sucon  4564  dtru  4571  0elsucexmid  4576  ordpwsucexmid  4581  ordtri2or2exmid  4582  ontri2orexmidim  4583  dcextest  4592  omex  4604  find  4610  omelon  4620  nnoni  4622  limom  4625  nnregexmid  4632  omsinds  4633  xpeq1i  4658  xpeq2i  4659  0nelxp  4666  opthprc  4689  mosubop  4704  releqi  4721  relssi  4729  relin1  4756  relin2  4757  reldif  4758  inopab  4771  difopab  4772  xpiindim  4776  opabbi2dv  4788  ideq  4791  coeq1i  4798  coeq2i  4799  cnveqi  4814  eldm  4836  eldm2  4837  dmeqi  4840  dmv  4855  rneqi  4867  elrnmpti  4892  dmex  4905  rnex  4906  reseq1i  4915  reseq2i  4916  residm  4951  resex  4960  resmpt3  4968  imaeq1i  4979  imaeq2i  4980  elima  4987  imaex  4995  elimasn  5007  args  5009  epini  5011  dfse2  5013  eliniseg2  5020  relbrcnv  5021  cotr  5022  issref  5023  cnvsym  5024  asymref  5026  intirr  5027  codir  5029  qfto  5030  ssrnres  5083  cnveq0  5097  cnvsn0  5109  dmsnop  5114  rnsnop  5121  resdm2  5131  dfco2a  5141  cocnvcnv1  5151  coi2  5157  coires1  5158  cnvssrndm  5162  cossxp  5163  cocnvres  5165  relrelss  5167  relcoi2  5171  unidmrn  5173  dfdm2  5175  unixpm  5176  cnvexg  5178  cnvex  5179  cnviinm  5182  iotaval  5201  funeqi  5249  funi  5260  funres  5269  funcnvsn  5273  funcnvcnv  5287  funin  5299  funcnvres  5301  isarep2  5315  fneq1i  5322  fneq2i  5323  fnresdisj  5338  fnresi  5345  mpt0  5355  dmmpti  5357  feq1i  5370  feq2i  5371  fdmi  5385  fun2  5401  fssres  5403  resasplitss  5407  fintm  5413  fconst6  5427  f1ores  5488  foimacnv  5491  resdif  5495  funcocnv2  5498  f1ovi  5512  fveq1i  5528  fveq2i  5530  0fv  5562  fvun1  5595  fvopab3ig  5603  fvmptss2  5604  mptrcl  5611  elfvmptrab1  5623  fndmdif  5634  fneqeql2  5638  f1oresrab  5694  fmptco  5695  fnressn  5715  fressnfv  5716  fmptap  5719  fvsnun1  5726  fvsnun2  5727  fsnunfv  5730  fconst2  5746  mptex  5755  riotabiia  5861  acexmidlema  5879  acexmidlemb  5880  acexmidlemcase  5883  acexmidlem2  5885  acexmidlemv  5886  oveq1i  5898  oveq2i  5899  oveqi  5901  oprabidlem  5919  0neqopab  5933  oprabbii  5943  oprabss  5974  mpompt  5980  funoprab  5988  fnoprab  5991  ovigg  6009  elmpocl  6083  resfunexgALT  6123  cofunexg  6124  mptexw  6128  opabex3d  6136  opabex3  6137  1st0  6159  2nd0  6160  op1st  6161  op2nd  6162  f1stres  6174  f2ndres  6175  fo1stresm  6176  fo2ndresm  6177  1stcof  6178  2ndcof  6179  1stexg  6182  2ndexg  6183  releldm2  6200  reldm  6201  dfoprab3  6206  mpomptsx  6212  mpompts  6213  fnmpoi  6219  dmmpo  6220  mpoexxg  6225  mpoexw  6228  1stconst  6236  2ndconst  6237  dfmpo  6238  algrflem  6244  algrflemg  6245  cnvoprab  6249  f1od2  6250  mpoxopn0yelv  6254  mpoxopoveq  6255  tposssxp  6264  brtpos2  6266  reldmtpos  6268  dftpos2  6276  dftpos4  6278  tpostpos  6279  tpostpos2  6280  tposfo  6286  tposf  6287  tposeqi  6292  tposex  6293  tposoprab  6295  issmo  6303  smores  6307  smores2  6309  iordsmo  6312  smo0  6313  tfrlem8  6333  tfrexlem  6349  tfr1onlem3  6353  tfr1onlemsucaccv  6356  tfr1onlembxssdm  6358  tfr1onlemres  6364  tfri1dALT  6366  tfri2  6381  rdgisuc1  6399  rdg0  6402  frecfun  6410  frec0g  6412  freccllem  6417  frecfcllem  6419  frecsuclem  6421  frecrdg  6423  2on0  6441  xp01disj  6448  2oconcl  6454  fnoa  6462  oaexg  6463  fnom  6465  omexg  6466  fnoei  6467  oeiexg  6468  oei0  6474  oacl  6475  oasuc  6479  o1p1e2  6483  omsuc  6487  nna0r  6493  nnm0r  6494  1onn  6535  2onn  6536  3onn  6537  4onn  6538  2ssom  6539  eqerlem  6580  elqs  6600  qsex  6606  ecqs  6611  iinerm  6621  th3qlem1  6651  th3q  6654  mapsn  6704  mapsnf1o3  6711  ixpiinm  6738  ixpssmap  6746  brdom  6764  f1dom  6774  enref  6779  dom2  6789  idssen  6791  ssdomg  6792  ensymi  6796  ensn1  6810  fiprc  6829  1domsn  6833  xpcomf1o  6839  xpcomco  6840  dom0  6852  0dom  6853  xpmapenlem  6863  phplem2  6867  php5  6872  snnen2og  6873  1nen2  6875  php5dom  6877  ssfilem  6889  ssfiexmid  6890  domfiexmid  6892  0fin  6898  diffitest  6901  findcard  6902  findcard2  6903  findcard2s  6904  isinfinf  6911  ac6sfi  6912  inffiexmid  6920  pw1fin  6924  unfiexmid  6931  xpfi  6943  fisseneq  6945  ssfirab  6947  en1eqsn  6961  snexxph  6963  sbthlem2  6971  sbthlemi3  6972  sbthlemi6  6975  sbthlem7  6976  fi0  6988  supeq1i  7001  infeq1i  7026  djuexb  7057  djuf1olemr  7067  inresflem  7073  djuinr  7076  updjudhcoinlf  7093  updjudhcoinrg  7094  casefun  7098  caserel  7100  caseinj  7102  caseinl  7104  caseinr  7105  omp1eomlem  7107  endjusym  7109  difinfsn  7113  difinfinf  7114  djuinj  7119  0ct  7120  ctmlemr  7121  ctssdclemn0  7123  ctssdccl  7124  omct  7130  ctfoex  7131  finomni  7152  exmidomni  7154  fodjuomni  7161  ctssexmid  7162  fodjumkv  7172  nninfwlporlem  7185  nninfwlpoimlemg  7187  nninfwlpoim  7190  card0  7201  exmidonfinlem  7206  dju1p1e2  7210  exmidfodomrlemim  7214  exmidfodomrlemr  7215  exmidfodomrlemrALT  7216  3nelsucpw1  7247  sucpw1nss3  7248  3nsssucpw1  7249  2onetap  7268  exmidmotap  7274  0npi  7326  dmaddpi  7338  dmmulpi  7339  1lt2pi  7353  0nnq  7377  1nq  7379  dmaddpq  7392  dmmulpq  7393  rec1nq  7408  1lt2nq  7419  halfnqq  7423  prarloclemarch2  7432  enq0enq  7444  nqnq0pi  7451  nnnq0lem1  7459  addnnnq0  7462  mulnnnq0  7463  nq0m0r  7469  addpinq1  7477  prarloclem5  7513  prarloclemcalc  7515  1pr  7567  1idprl  7603  1idpru  7604  ltexprlemm  7613  recexprlem1ssl  7646  recexprlem1ssu  7647  suplocexprlemell  7726  suplocexprlem2b  7727  suplocexprlemmu  7731  suplocexprlemdisj  7733  suplocexprlemloc  7734  suplocexprlemub  7736  suplocexprlemlub  7737  prsrlem1  7755  addsrpr  7758  mulsrpr  7759  gt0srpr  7761  0nsr  7762  0r  7763  1sr  7764  m1r  7765  m1m1sr  7774  caucvgsr  7815  suplocsrlempr  7820  addresr  7850  mulresr  7851  pitonnlem1  7858  peano1nnnn  7865  axi2m1  7888  axcnre  7894  peano5nnnn  7905  axcaucvg  7913  mulid1i  7973  mullidi  7974  pnfnre  8013  mnfnre  8014  pnfnemnf  8026  mnfxr  8028  rexri  8029  ltnri  8064  ltleii  8074  00id  8112  addid1i  8113  addid2i  8114  0cnALT  8161  negeqi  8165  negicn  8172  neg0  8217  renegcli  8233  negcli  8239  negidi  8240  negnegi  8241  subidi  8242  subid1i  8243  negne0bi  8244  negrebi  8245  mul02i  8361  mul01i  8362  mulm1i  8374  leidi  8456  gt0ne0ii  8458  inelr  8555  msqge0i  8588  gt0ap0ii  8599  1div1e1  8675  div1i  8711  eqnegi  8712  recclapi  8713  recidapi  8714  divmulapi  8737  rerecclapi  8748  redivclapi  8750  rerecapb  8814  recgt0  8821  ltp1i  8876  divgt0ii  8890  ltmul1ii  8899  ltdiv1ii  8900  sup3exmid  8928  peano5nni  8936  nnrei  8942  1nn  8944  nngt0i  8963  neg1ap0  9042  2timesi  9063  times2i  9064  2nn  9094  3nn  9095  4nn  9096  5nn  9097  6nn  9098  7nn  9099  8nn  9100  9nn  9101  2muline0  9158  rehalfcli  9181  nn0ssre  9194  nnnn0i  9198  dfn2  9203  0nn0  9205  nn0ge0i  9217  zrei  9273  neg1z  9299  nn0negzi  9302  dfz2  9339  nneoi  9371  peano5uzi  9376  dfuzi  9377  nn0ind-raph  9384  deceq1i  9404  deceq2i  9405  10nn  9413  numltc  9423  eluzel2  9547  eluz1i  9549  nn0uz  9576  nnuz  9577  infrenegsupex  9608  lbzbi  9630  divfnzn  9635  qdivcl  9657  irrmul  9661  cnref1o  9664  0ltpnf  9796  mnflt0  9798  0lepnf  9804  xrltnsym  9807  xrlttri3  9811  nltpnft  9828  ngtmnft  9831  xrrebnd  9833  xnegmnf  9843  xneg0  9845  xltnegi  9849  xaddmnf1  9862  xaddmnf2  9863  mnfaddpnf  9865  xaddid1  9876  xnn0lenn0nn0  9879  xnn0xadd0  9881  xposdif  9896  ixxex  9913  iooval2  9929  unirnioo  9987  ioorebasg  9989  elrege0  9990  fzval2  10025  fzen  10057  fzprval  10096  fztpval  10097  uzdisj  10107  ige2m1fz  10124  fz01or  10125  fz1ssfz0  10131  fz0sn  10135  fz0tp  10136  fz0to3un2pr  10137  fz0to4untppr  10138  nn0disj  10152  1fv  10153  4fvwrd4  10154  fzo0ss1  10188  fzo01  10230  fzo12sn  10231  fzo0to2pr  10232  fzo0to3tp  10233  fzo0to42pr  10234  qbtwnxr  10272  flval  10286  modqfrac  10351  modqmulnn  10356  q2txmodxeq0  10398  frecuzrdgdom  10432  frecuzrdgfun  10434  frecuzrdgsuct  10438  frechashgf1o  10442  nnct  10449  fxnn0nninf  10452  0tonninf  10453  1tonninf  10454  iseqvalcbv  10471  ser0f  10529  0exp0e1  10539  qexpcl  10550  qexpclz  10555  m1expcl2  10556  1exp  10563  sqvali  10614  sqcli  10615  sqeq0i  10616  resqcli  10619  sq1  10628  neg1sqe1  10629  iexpcyc  10639  qsqeqor  10645  facnn  10721  fac0  10722  fac1  10723  fac2  10725  fac3  10726  fac4  10727  bcval  10743  bcm1k  10754  bcpasc  10760  bccl  10761  4bc3eq4  10767  4bc2eq6  10768  hashinfom  10772  hashennn  10774  hashfz1  10777  fihasheq0  10787  hash0  10790  hashsng  10792  fihashen1  10793  omgadd  10796  hashp1i  10804  hashxp  10820  fimaxq  10821  zfz1iso  10835  shftidt2  10855  cjexp  10916  re0  10918  im0  10919  re1  10920  im1  10921  cj0  10924  cji  10925  recli  10934  imcli  10935  cjcli  10936  replimi  10937  cjcji  10938  reim0bi  10939  rerebi  10940  cjrebi  10941  recji  10942  imcji  10943  cjmulrcli  10944  cjmulvali  10945  cjmulge0i  10946  renegi  10947  imnegi  10948  cjnegi  10949  addcji  10950  uzin2  11010  rexanuz  11011  rexfiuz  11012  sqrtrval  11023  sqrt0  11027  resqrexlemcalc3  11039  resqrexlemcvg  11042  resqrex  11049  abs0  11081  absi  11082  qabsor  11098  absimle  11107  recan  11132  caubnd2  11140  leabsi  11151  absrei  11152  sqrtpclii  11153  sqrtgt0ii  11154  absvalsqi  11163  absvalsq2i  11164  abscli  11165  absge0i  11166  absval2i  11167  abs00i  11168  absgt0api  11169  absnegi  11170  abscji  11171  releabsi  11172  infxrnegsupex  11285  xrbdtri  11298  cbvsum  11382  sumeq1i  11385  sum0  11410  isumz  11411  fisumss  11414  fsumsersdc  11417  fsumadd  11428  isumclim  11443  isumclim3  11445  fsumcnv  11459  modfsummodlem1  11478  fsumrelem  11493  binomlem  11505  binom  11506  arisum2  11521  expcnv  11526  0.999...  11543  prodf1f  11565  cbvprod  11580  prodeq1i  11583  zproddc  11601  zprodap0  11603  prod0  11607  fprodssdc  11612  prodsnf  11614  fprodcnv  11647  fprodge0  11659  fprodge1  11661  ef0lem  11682  esum  11684  ere  11692  ege2le3  11693  ef0  11694  eff2  11702  efsep  11713  reeff1  11722  sin0  11751  cos0  11752  ef01bndlem  11778  cos2bnd  11782  sincos1sgn  11786  sincos2sgn  11787  sin4lt0  11788  eirr  11800  0dvds  11832  dvds1  11873  z0even  11930  n2dvdsm1  11932  z2even  11933  n2dvds3  11934  ndvdssub  11949  ndvdsi  11952  flodddiv4  11953  zsupssdc  11969  gcddvds  11978  gcd1  12002  6gcd4e2  12010  bezoutlembi  12020  dfgcd3  12025  dfgcd2  12029  lcmval  12077  lcmcllem  12081  lcmledvds  12084  3lcm2e6woprm  12100  qredeu  12111  isprm2lem  12130  isprm3  12132  prm2orodd  12140  isprm5lem  12155  sqrt2irr0  12178  pw2dvds  12180  phicl2  12228  phi1  12233  dfphi2  12234  phiprmpw  12236  eulerthlemrprm  12243  eulerthlemh  12245  odzval  12255  oddprm  12273  pczpre  12311  pcdiv  12316  pc0  12318  pcqdiv  12321  pcrec  12322  pcexp  12323  pcxcl  12325  pcdvdstr  12340  pc2dvds  12343  dvdsprmpweqnn  12349  pcmpt  12355  qexpz  12364  pockthi  12370  1arith2  12380  ennnfonelemp1  12421  ennnfonelem1  12422  ennnfonelemkh  12427  ennnfonelemex  12429  ennnfonelemnn0  12437  ennnfonelemr  12438  exmidunben  12441  ctinfomlemom  12442  ctinfom  12443  ctinf  12445  qnnen  12446  omctfn  12458  omiunct  12459  ssnnctlemct  12461  nninfdc  12468  structcnvcnv  12492  structfun  12494  structfn  12495  ndxarg  12499  ndxid  12500  setsresg  12514  setsslnid  12528  basmex  12535  basmexd  12536  strleun  12578  strle1g  12580  prdsex  12736  imasaddfnlemg  12753  quslem  12763  xpsfrnel  12782  xpsff1o  12787  ismgmn0  12796  fn0g  12813  0g0  12814  rmodislmodlem  13539  rmodislmod  13540  lidlmex  13664  cnfldex  13740  cnfldbas  13741  cnfldadd  13742  cnfldmul  13743  cnfldcj  13744  cnring  13746  cnfld0  13747  cnfld1  13748  cnfldneg  13749  cnfldplusf  13750  cnfldsub  13751  cnfldmulg  13752  cnfldexp  13753  cnsubglem  13755  cnsubrglem  13756  gzsubrg  13758  zringring  13765  zringabl  13766  zringgrp  13767  zring1  13773  zringsubgval  13777  istopon  13809  topontopi  13812  toponunii  13813  toponrestid  13817  istps  13828  topontopn  13833  eltpsi  13837  eltg4i  13851  eltg3  13853  tg1  13855  tg2  13856  tgclb  13861  topnex  13882  sn0topon  13884  distps  13887  cldrcl  13898  sn0cld  13933  restco  13970  lmrcl  13987  ssidcn  14006  cnconst2  14029  cnptopresti  14034  cnptoprest  14035  txuni2  14052  txbas  14054  eltx  14055  txcnp  14067  upxp  14068  txcnmpt  14069  uptx  14070  txcn  14071  txrest  14072  txlm  14075  cnmptid  14077  cnmpt1st  14084  cnmpt2nd  14085  hmeofn  14098  psmetge0  14127  ismeti  14142  xmetunirn  14154  xmetge0  14161  unirnblps  14218  unirnbl  14219  mopnex  14301  qtopbasss  14317  retop  14320  uniretop  14321  iooretopg  14324  cnxmet  14327  cntoptopon  14328  cnbl0  14330  rexmet  14337  blssioo  14341  tgioo  14342  tgqioo  14343  cnopnap  14390  limcresi  14431  dvfvalap  14446  dvidlemap  14456  dvcnp2cntop  14459  dvcoapbr  14467  dvexp2  14472  dvrecap  14473  dveflem  14483  dvef  14484  reeff1o  14490  sin0pilem1  14498  sin0pilem2  14499  pilem3  14500  pigt2lt4  14501  pire  14503  sinhalfpilem  14508  pidiv2halves  14512  cosneghalfpi  14515  cospi  14517  efipi  14518  sin2pi  14520  cos2pi  14521  ef2pi  14522  cosq14gt0  14549  coseq00topi  14552  coseq0negpitopi  14553  sincos4thpi  14557  sincos6thpi  14559  sincos3rdpi  14560  pigt3  14561  cos02pilt1  14568  ioocosf1o  14571  dfrelog  14577  relogf1o  14578  relogcl  14579  relogiso  14590  rpcxpsqrt  14638  rpabscxpbnd  14655  2logb9irr  14685  2logb9irrALT  14688  sqrt2cxp2logb9e3  14689  2irrexpq  14690  2logb9irrap  14691  2irrexpqap  14692  lgsdir2lem1  14725  lgsdir2lem2  14726  lgsdir2lem4  14728  lgsdir2lem5  14729  lgsdi  14734  m1lgs  14748  2lgsoddprmlem2  14750  2lgsoddprmlem3c  14753  2lgsoddprmlem3d  14754  2sqlem9  14767  2sqlem10  14768  ex-fl  14773  ex-ceil  14774  ex-exp  14775  ex-fac  14776  ex-gcd  14779  bj-stfal  14790  bj-stst  14793  bj-dcfal  14803  bj-dcdc  14807  bj-stdc  14808  bj-dcst  14809  bj-el2oss1o  14822  elabf2  14830  bd0  14872  bdeli  14894  bdcriota  14931  bdbm1.3ii  14939  bdinex1  14947  bdssexi  14951  bj-inex  14955  bj-snex  14961  bj-sucex  14971  bj-d0clsepcl  14973  bj-omind  14982  bj-om  14985  bj-2inf  14986  bj-peano2  14987  bdpeano5  14991  bj-omssonALT  15011  bj-inf2vnlem1  15018  bj-omex2  15025  bj-nn0sucALT  15026  012of  15042  2o01f  15043  subctctexmid  15047  nninfall  15055  nninfsellemqall  15061  nninfsellemeqinf  15062  nninfomnilem  15064  nninfomni  15065  exmidsbthrlem  15067  sbthom  15071  isomninnlem  15075  isomninn  15076  cvgcmp2nlemabs  15077  iooreen  15080  trilpolemisumle  15083  trilpolemeq1  15085  trilpo  15088  trirec0  15089  apdifflemr  15092  iswomninnlem  15094  iswomninn  15095  ismkvnnlem  15097  ismkvnn  15098  redcwlpo  15100  dcapnconst  15106  nconstwlpolem0  15108  nconstwlpo  15111  neapmkv  15113  neap0mkv  15114  taupi  15118