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  2676  rexeqi  2677  rabeqif  2728  elv  2741  elexi  2749  ceqsal  2766  vtocl3  2793  vtoclef  2810  vtocle  2811  spcv  2831  spcev  2832  clel3  2872  elabf  2880  elab2  2885  elab3  2889  euxfrdc  2923  reueq  2936  rmoimi2  2940  sbsbc  2966  sbc8g  2970  sbc6  2988  sbcie  2997  sbcrex  3042  csbvarg  3085  csbief  3101  csbie2  3106  sbnfc2  3117  sseli  3151  sselii  3152  sseq1i  3181  sseq2i  3182  difeq1i  3249  difeq2i  3250  uneq1i  3285  uneq2i  3286  ineq1i  3332  ineq2i  3333  ssinss1  3364  difdif2ss  3392  n0ii  3431  ne0ii  3432  vn0  3433  vn0m  3434  abf  3466  disj2  3478  difid  3491  0dif  3494  disjdif  3495  difin0  3496  undif1ss  3497  difdifdirss  3507  rgenm  3525  iftruei  3540  iffalsei  3543  ifbieq2i  3557  ifbieq12i  3559  pweqi  3579  pwid  3590  sneqi  3604  elsn  3608  elpr  3613  elsn2  3626  ralsn  3635  rexsn  3636  eltp  3640  rabrsndc  3660  preq1i  3672  preq2i  3673  prid1  3698  snnz  3711  snm  3712  prnz  3714  prm  3715  tpnz  3717  snss  3727  snsssn  3761  opeq1i  3781  opeq2i  3782  unieqi  3819  unissi  3832  inteqi  3848  intmin2  3870  intab  3873  intsn  3879  iinconstm  3895  iuniin  3896  iinss1  3898  iunxdif2  3935  ssiinf  3936  iinss  3938  iinss2  3939  iinab  3948  iundif2ss  3952  iindif2m  3954  iinin2m  3955  iunxsn  3963  iunxprg  3967  iinpw  3977  sndisj  3999  disjxsn  4001  breqi  4009  breq1i  4010  breq2i  4011  brab1  4050  opabbii  4070  truni  4115  bm1.3ii  4124  a9evsep  4125  ax9vsep  4126  zfnuleu  4127  axnul  4128  ssexi  4141  rabex  4147  elpw2  4157  pwnss  4159  iin0r  4169  intv  4170  pwex  4183  snex  4185  notnotsnex  4187  ord3ex  4190  dtruarb  4191  undifexmid  4193  intid  4224  opnzi  4235  copsexg  4244  opelopabf  4274  epelc  4291  elon  4374  inton  4393  onn0  4400  onm  4401  elsuc  4406  elsuc2  4407  sucid  4417  iunsuc  4420  onordi  4426  ontrci  4427  onelssi  4429  eusvnf  4453  ssonunii  4488  sucex  4498  onssi  4514  onsuci  4515  ordtriexmidlem  4518  ordtriexmidlem2  4519  ordtriexmid  4520  ontriexmidim  4521  ordtri2orexmid  4522  2ordpr  4523  ontr2exmid  4524  onsucsssucexmid  4526  onsucelsucexmid  4529  regexmidlemm  4531  reg2exmid  4535  onirri  4542  ruALT  4550  onprc  4551  sucon  4552  dtru  4559  0elsucexmid  4564  ordpwsucexmid  4569  ordtri2or2exmid  4570  ontri2orexmidim  4571  dcextest  4580  omex  4592  find  4598  omelon  4608  nnoni  4610  limom  4613  nnregexmid  4620  omsinds  4621  xpeq1i  4646  xpeq2i  4647  0nelxp  4654  opthprc  4677  mosubop  4692  releqi  4709  relssi  4717  relin1  4744  relin2  4745  reldif  4746  inopab  4759  difopab  4760  xpiindim  4764  opabbi2dv  4776  ideq  4779  coeq1i  4786  coeq2i  4787  cnveqi  4802  eldm  4824  eldm2  4825  dmeqi  4828  dmv  4843  rneqi  4855  elrnmpti  4880  dmex  4893  rnex  4894  reseq1i  4903  reseq2i  4904  residm  4939  resex  4948  resmpt3  4956  imaeq1i  4967  imaeq2i  4968  elima  4975  imaex  4983  elimasn  4995  args  4997  epini  4999  dfse2  5001  eliniseg2  5008  relbrcnv  5009  cotr  5010  issref  5011  cnvsym  5012  asymref  5014  intirr  5015  codir  5017  qfto  5018  ssrnres  5071  cnveq0  5085  cnvsn0  5097  dmsnop  5102  rnsnop  5109  resdm2  5119  dfco2a  5129  cocnvcnv1  5139  coi2  5145  coires1  5146  cnvssrndm  5150  cossxp  5151  cocnvres  5153  relrelss  5155  relcoi2  5159  unidmrn  5161  dfdm2  5163  unixpm  5164  cnvexg  5166  cnvex  5167  cnviinm  5170  iotaval  5189  funeqi  5237  funi  5248  funres  5257  funcnvsn  5261  funcnvcnv  5275  funin  5287  funcnvres  5289  isarep2  5303  fneq1i  5310  fneq2i  5311  fnresdisj  5326  fnresi  5333  mpt0  5343  dmmpti  5345  feq1i  5358  feq2i  5359  fdmi  5373  fun2  5389  fssres  5391  resasplitss  5395  fintm  5401  fconst6  5415  f1ores  5476  foimacnv  5479  resdif  5483  funcocnv2  5486  f1ovi  5500  fveq1i  5516  fveq2i  5518  0fv  5550  fvun1  5582  fvopab3ig  5590  fvmptss2  5591  mptrcl  5598  elfvmptrab1  5610  fndmdif  5621  fneqeql2  5625  f1oresrab  5681  fmptco  5682  fnressn  5702  fressnfv  5703  fmptap  5706  fvsnun1  5713  fvsnun2  5714  fsnunfv  5717  fconst2  5733  mptex  5742  riotabiia  5847  acexmidlema  5865  acexmidlemb  5866  acexmidlemcase  5869  acexmidlem2  5871  acexmidlemv  5872  oveq1i  5884  oveq2i  5885  oveqi  5887  oprabidlem  5905  0neqopab  5919  oprabbii  5929  oprabss  5960  mpompt  5966  funoprab  5974  fnoprab  5977  fovcl  5979  ovigg  5994  elmpocl  6068  resfunexgALT  6108  cofunexg  6109  mptexw  6113  opabex3d  6121  opabex3  6122  1st0  6144  2nd0  6145  op1st  6146  op2nd  6147  f1stres  6159  f2ndres  6160  fo1stresm  6161  fo2ndresm  6162  1stcof  6163  2ndcof  6164  1stexg  6167  2ndexg  6168  releldm2  6185  reldm  6186  dfoprab3  6191  mpomptsx  6197  mpompts  6198  fnmpoi  6204  dmmpo  6205  mpoexxg  6210  mpoexw  6213  1stconst  6221  2ndconst  6222  dfmpo  6223  algrflem  6229  algrflemg  6230  cnvoprab  6234  f1od2  6235  mpoxopn0yelv  6239  mpoxopoveq  6240  tposssxp  6249  brtpos2  6251  reldmtpos  6253  dftpos2  6261  dftpos4  6263  tpostpos  6264  tpostpos2  6265  tposfo  6271  tposf  6272  tposeqi  6277  tposex  6278  tposoprab  6280  issmo  6288  smores  6292  smores2  6294  iordsmo  6297  smo0  6298  tfrlem8  6318  tfrexlem  6334  tfr1onlem3  6338  tfr1onlemsucaccv  6341  tfr1onlembxssdm  6343  tfr1onlemres  6349  tfri1dALT  6351  tfri2  6366  rdgisuc1  6384  rdg0  6387  frecfun  6395  frec0g  6397  freccllem  6402  frecfcllem  6404  frecsuclem  6406  frecrdg  6408  2on0  6426  xp01disj  6433  2oconcl  6439  fnoa  6447  oaexg  6448  fnom  6450  omexg  6451  fnoei  6452  oeiexg  6453  oei0  6459  oacl  6460  oasuc  6464  o1p1e2  6468  omsuc  6472  nna0r  6478  nnm0r  6479  1onn  6520  2onn  6521  3onn  6522  4onn  6523  2ssom  6524  eqerlem  6565  elqs  6585  qsex  6591  ecqs  6596  iinerm  6606  th3qlem1  6636  th3q  6639  mapsn  6689  mapsnf1o3  6696  ixpiinm  6723  ixpssmap  6731  brdom  6749  f1dom  6759  enref  6764  dom2  6774  idssen  6776  ssdomg  6777  ensymi  6781  ensn1  6795  fiprc  6814  1domsn  6818  xpcomf1o  6824  xpcomco  6825  dom0  6837  0dom  6838  xpmapenlem  6848  phplem2  6852  php5  6857  snnen2og  6858  1nen2  6860  php5dom  6862  ssfilem  6874  ssfiexmid  6875  domfiexmid  6877  0fin  6883  diffitest  6886  findcard  6887  findcard2  6888  findcard2s  6889  isinfinf  6896  ac6sfi  6897  inffiexmid  6905  pw1fin  6909  unfiexmid  6916  xpfi  6928  fisseneq  6930  ssfirab  6932  en1eqsn  6946  snexxph  6948  sbthlem2  6956  sbthlemi3  6957  sbthlemi6  6960  sbthlem7  6961  fi0  6973  supeq1i  6986  infeq1i  7011  djuexb  7042  djuf1olemr  7052  inresflem  7058  djuinr  7061  updjudhcoinlf  7078  updjudhcoinrg  7079  casefun  7083  caserel  7085  caseinj  7087  caseinl  7089  caseinr  7090  omp1eomlem  7092  endjusym  7094  difinfsn  7098  difinfinf  7099  djuinj  7104  0ct  7105  ctmlemr  7106  ctssdclemn0  7108  ctssdccl  7109  omct  7115  ctfoex  7116  finomni  7137  exmidomni  7139  fodjuomni  7146  ctssexmid  7147  fodjumkv  7157  nninfwlporlem  7170  nninfwlpoimlemg  7172  nninfwlpoim  7175  card0  7186  exmidonfinlem  7191  dju1p1e2  7195  exmidfodomrlemim  7199  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  3nelsucpw1  7232  sucpw1nss3  7233  3nsssucpw1  7234  2onetap  7253  exmidmotap  7259  0npi  7311  dmaddpi  7323  dmmulpi  7324  1lt2pi  7338  0nnq  7362  1nq  7364  dmaddpq  7377  dmmulpq  7378  rec1nq  7393  1lt2nq  7404  halfnqq  7408  prarloclemarch2  7417  enq0enq  7429  nqnq0pi  7436  nnnq0lem1  7444  addnnnq0  7447  mulnnnq0  7448  nq0m0r  7454  addpinq1  7462  prarloclem5  7498  prarloclemcalc  7500  1pr  7552  1idprl  7588  1idpru  7589  ltexprlemm  7598  recexprlem1ssl  7631  recexprlem1ssu  7632  suplocexprlemell  7711  suplocexprlem2b  7712  suplocexprlemmu  7716  suplocexprlemdisj  7718  suplocexprlemloc  7719  suplocexprlemub  7721  suplocexprlemlub  7722  prsrlem1  7740  addsrpr  7743  mulsrpr  7744  gt0srpr  7746  0nsr  7747  0r  7748  1sr  7749  m1r  7750  m1m1sr  7759  caucvgsr  7800  suplocsrlempr  7805  addresr  7835  mulresr  7836  pitonnlem1  7843  peano1nnnn  7850  axi2m1  7873  axcnre  7879  peano5nnnn  7890  axcaucvg  7898  mulid1i  7958  mullidi  7959  pnfnre  7998  mnfnre  7999  pnfnemnf  8011  mnfxr  8013  rexri  8014  ltnri  8049  ltleii  8059  00id  8097  addid1i  8098  addid2i  8099  0cnALT  8146  negeqi  8150  negicn  8157  neg0  8202  renegcli  8218  negcli  8224  negidi  8225  negnegi  8226  subidi  8227  subid1i  8228  negne0bi  8229  negrebi  8230  mul02i  8346  mul01i  8347  mulm1i  8359  leidi  8441  gt0ne0ii  8443  inelr  8540  msqge0i  8573  gt0ap0ii  8584  1div1e1  8660  div1i  8696  eqnegi  8697  recclapi  8698  recidapi  8699  divmulapi  8722  rerecclapi  8733  redivclapi  8735  rerecapb  8799  recgt0  8806  ltp1i  8861  divgt0ii  8875  ltmul1ii  8884  ltdiv1ii  8885  sup3exmid  8913  peano5nni  8921  nnrei  8927  1nn  8929  nngt0i  8948  neg1ap0  9027  2timesi  9048  times2i  9049  2nn  9079  3nn  9080  4nn  9081  5nn  9082  6nn  9083  7nn  9084  8nn  9085  9nn  9086  2muline0  9143  rehalfcli  9166  nn0ssre  9179  nnnn0i  9183  dfn2  9188  0nn0  9190  nn0ge0i  9202  zrei  9258  neg1z  9284  nn0negzi  9287  dfz2  9324  nneoi  9356  peano5uzi  9361  dfuzi  9362  nn0ind-raph  9369  deceq1i  9389  deceq2i  9390  10nn  9398  numltc  9408  eluzel2  9532  eluz1i  9534  nn0uz  9561  nnuz  9562  infrenegsupex  9593  lbzbi  9615  divfnzn  9620  qdivcl  9642  irrmul  9646  cnref1o  9649  0ltpnf  9781  mnflt0  9783  0lepnf  9789  xrltnsym  9792  xrlttri3  9796  nltpnft  9813  ngtmnft  9816  xrrebnd  9818  xnegmnf  9828  xneg0  9830  xltnegi  9834  xaddmnf1  9847  xaddmnf2  9848  mnfaddpnf  9850  xaddid1  9861  xnn0lenn0nn0  9864  xnn0xadd0  9866  xposdif  9881  ixxex  9898  iooval2  9914  unirnioo  9972  ioorebasg  9974  elrege0  9975  fzval2  10010  fzen  10042  fzprval  10081  fztpval  10082  uzdisj  10092  ige2m1fz  10109  fz01or  10110  fz1ssfz0  10116  fz0sn  10120  fz0tp  10121  fz0to3un2pr  10122  fz0to4untppr  10123  nn0disj  10137  1fv  10138  4fvwrd4  10139  fzo0ss1  10173  fzo01  10215  fzo12sn  10216  fzo0to2pr  10217  fzo0to3tp  10218  fzo0to42pr  10219  qbtwnxr  10257  flval  10271  modqfrac  10336  modqmulnn  10341  q2txmodxeq0  10383  frecuzrdgdom  10417  frecuzrdgfun  10419  frecuzrdgsuct  10423  frechashgf1o  10427  nnct  10434  fxnn0nninf  10437  0tonninf  10438  1tonninf  10439  iseqvalcbv  10456  ser0f  10514  0exp0e1  10524  qexpcl  10535  qexpclz  10540  m1expcl2  10541  1exp  10548  sqvali  10599  sqcli  10600  sqeq0i  10601  resqcli  10604  sq1  10613  neg1sqe1  10614  iexpcyc  10624  qsqeqor  10630  facnn  10706  fac0  10707  fac1  10708  fac2  10710  fac3  10711  fac4  10712  bcval  10728  bcm1k  10739  bcpasc  10745  bccl  10746  4bc3eq4  10752  4bc2eq6  10753  hashinfom  10757  hashennn  10759  hashfz1  10762  fihasheq0  10772  hash0  10775  hashsng  10777  fihashen1  10778  omgadd  10781  hashp1i  10789  hashxp  10805  fimaxq  10806  zfz1iso  10820  shftidt2  10840  cjexp  10901  re0  10903  im0  10904  re1  10905  im1  10906  cj0  10909  cji  10910  recli  10919  imcli  10920  cjcli  10921  replimi  10922  cjcji  10923  reim0bi  10924  rerebi  10925  cjrebi  10926  recji  10927  imcji  10928  cjmulrcli  10929  cjmulvali  10930  cjmulge0i  10931  renegi  10932  imnegi  10933  cjnegi  10934  addcji  10935  uzin2  10995  rexanuz  10996  rexfiuz  10997  sqrtrval  11008  sqrt0  11012  resqrexlemcalc3  11024  resqrexlemcvg  11027  resqrex  11034  abs0  11066  absi  11067  qabsor  11083  absimle  11092  recan  11117  caubnd2  11125  leabsi  11136  absrei  11137  sqrtpclii  11138  sqrtgt0ii  11139  absvalsqi  11148  absvalsq2i  11149  abscli  11150  absge0i  11151  absval2i  11152  abs00i  11153  absgt0api  11154  absnegi  11155  abscji  11156  releabsi  11157  infxrnegsupex  11270  xrbdtri  11283  cbvsum  11367  sumeq1i  11370  sum0  11395  isumz  11396  fisumss  11399  fsumsersdc  11402  fsumadd  11413  isumclim  11428  isumclim3  11430  fsumcnv  11444  modfsummodlem1  11463  fsumrelem  11478  binomlem  11490  binom  11491  arisum2  11506  expcnv  11511  0.999...  11528  prodf1f  11550  cbvprod  11565  prodeq1i  11568  zproddc  11586  zprodap0  11588  prod0  11592  fprodssdc  11597  prodsnf  11599  fprodcnv  11632  fprodge0  11644  fprodge1  11646  ef0lem  11667  esum  11669  ere  11677  ege2le3  11678  ef0  11679  eff2  11687  efsep  11698  reeff1  11707  sin0  11736  cos0  11737  ef01bndlem  11763  cos2bnd  11767  sincos1sgn  11771  sincos2sgn  11772  sin4lt0  11773  eirr  11785  0dvds  11817  dvds1  11858  z0even  11915  n2dvdsm1  11917  z2even  11918  n2dvds3  11919  ndvdssub  11934  ndvdsi  11937  flodddiv4  11938  zsupssdc  11954  gcddvds  11963  gcd1  11987  6gcd4e2  11995  bezoutlembi  12005  dfgcd3  12010  dfgcd2  12014  lcmval  12062  lcmcllem  12066  lcmledvds  12069  3lcm2e6woprm  12085  qredeu  12096  isprm2lem  12115  isprm3  12117  prm2orodd  12125  isprm5lem  12140  sqrt2irr0  12163  pw2dvds  12165  phicl2  12213  phi1  12218  dfphi2  12219  phiprmpw  12221  eulerthlemrprm  12228  eulerthlemh  12230  odzval  12240  oddprm  12258  pczpre  12296  pcdiv  12301  pc0  12303  pcqdiv  12306  pcrec  12307  pcexp  12308  pcxcl  12310  pcdvdstr  12325  pc2dvds  12328  dvdsprmpweqnn  12334  pcmpt  12340  qexpz  12349  pockthi  12355  1arith2  12365  ennnfonelemp1  12406  ennnfonelem1  12407  ennnfonelemkh  12412  ennnfonelemex  12414  ennnfonelemnn0  12422  ennnfonelemr  12423  exmidunben  12426  ctinfomlemom  12427  ctinfom  12428  ctinf  12430  qnnen  12431  omctfn  12443  omiunct  12444  ssnnctlemct  12446  nninfdc  12453  structcnvcnv  12477  structfun  12479  structfn  12480  ndxarg  12484  ndxid  12485  setsresg  12499  setsslnid  12513  basmex  12520  basmexd  12521  strleun  12562  strle1g  12564  prdsex  12717  imasaddfnlemg  12734  quslem  12744  xpsfrnel  12762  xpsff1o  12767  ismgmn0  12776  fn0g  12793  0g0  12794  cnfldex  13428  cnfldbas  13429  cnfldadd  13430  cnfldmul  13431  cnfldcj  13432  cnring  13434  cnfld0  13435  cnfld1  13436  cnfldneg  13437  cnfldplusf  13438  cnfldsub  13439  cnfldmulg  13440  cnfldexp  13441  cnsubglem  13443  cnsubrglem  13444  gzsubrg  13446  zringring  13453  zringabl  13454  zringgrp  13455  zring1  13461  zringsubgval  13465  istopon  13483  topontopi  13486  toponunii  13487  toponrestid  13491  istps  13502  topontopn  13507  eltpsi  13511  eltg4i  13525  eltg3  13527  tg1  13529  tg2  13530  tgclb  13535  topnex  13556  sn0topon  13558  distps  13561  cldrcl  13572  sn0cld  13607  restco  13644  lmrcl  13661  ssidcn  13680  cnconst2  13703  cnptopresti  13708  cnptoprest  13709  txuni2  13726  txbas  13728  eltx  13729  txcnp  13741  upxp  13742  txcnmpt  13743  uptx  13744  txcn  13745  txrest  13746  txlm  13749  cnmptid  13751  cnmpt1st  13758  cnmpt2nd  13759  hmeofn  13772  psmetge0  13801  ismeti  13816  xmetunirn  13828  xmetge0  13835  unirnblps  13892  unirnbl  13893  mopnex  13975  qtopbasss  13991  retop  13994  uniretop  13995  iooretopg  13998  cnxmet  14001  cntoptopon  14002  cnbl0  14004  rexmet  14011  blssioo  14015  tgioo  14016  tgqioo  14017  cnopnap  14064  limcresi  14105  dvfvalap  14120  dvidlemap  14130  dvcnp2cntop  14133  dvcoapbr  14141  dvexp2  14146  dvrecap  14147  dveflem  14157  dvef  14158  reeff1o  14164  sin0pilem1  14172  sin0pilem2  14173  pilem3  14174  pigt2lt4  14175  pire  14177  sinhalfpilem  14182  pidiv2halves  14186  cosneghalfpi  14189  cospi  14191  efipi  14192  sin2pi  14194  cos2pi  14195  ef2pi  14196  cosq14gt0  14223  coseq00topi  14226  coseq0negpitopi  14227  sincos4thpi  14231  sincos6thpi  14233  sincos3rdpi  14234  pigt3  14235  cos02pilt1  14242  ioocosf1o  14245  dfrelog  14251  relogf1o  14252  relogcl  14253  relogiso  14264  rpcxpsqrt  14312  rpabscxpbnd  14329  2logb9irr  14359  2logb9irrALT  14362  sqrt2cxp2logb9e3  14363  2irrexpq  14364  2logb9irrap  14365  2irrexpqap  14366  lgsdir2lem1  14399  lgsdir2lem2  14400  lgsdir2lem4  14402  lgsdir2lem5  14403  lgsdi  14408  m1lgs  14422  2lgsoddprmlem2  14424  2lgsoddprmlem3c  14427  2lgsoddprmlem3d  14428  2sqlem9  14441  2sqlem10  14442  ex-fl  14447  ex-ceil  14448  ex-exp  14449  ex-fac  14450  ex-gcd  14453  bj-stfal  14464  bj-stst  14467  bj-dcfal  14477  bj-dcdc  14481  bj-stdc  14482  bj-dcst  14483  bj-el2oss1o  14496  elabf2  14504  bd0  14546  bdeli  14568  bdcriota  14605  bdbm1.3ii  14613  bdinex1  14621  bdssexi  14625  bj-inex  14629  bj-snex  14635  bj-sucex  14645  bj-d0clsepcl  14647  bj-omind  14656  bj-om  14659  bj-2inf  14660  bj-peano2  14661  bdpeano5  14665  bj-omssonALT  14685  bj-inf2vnlem1  14692  bj-omex2  14699  bj-nn0sucALT  14700  012of  14715  2o01f  14716  subctctexmid  14720  nninfall  14728  nninfsellemqall  14734  nninfsellemeqinf  14735  nninfomnilem  14737  nninfomni  14738  exmidsbthrlem  14740  sbthom  14744  isomninnlem  14748  isomninn  14749  cvgcmp2nlemabs  14750  iooreen  14753  trilpolemisumle  14756  trilpolemeq1  14758  trilpo  14761  trirec0  14762  apdifflemr  14765  iswomninnlem  14767  iswomninn  14768  ismkvnnlem  14770  ismkvnn  14771  redcwlpo  14773  dcapnconst  14778  nconstwlpolem0  14780  nconstwlpo  14783  neapmkv  14785  neap0mkv  14786  taupi  14790