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

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  110  simpri  112  biimpi  119  bicomi  131  mpbi  144  mpbir  145  imbi1i  237  a1bi  242  tbt  246  biantru  300  biantrur  301  mp2an  424  pm2.65i  634  notnoti  640  pm2.21i  641  pm2.24ii  642  notbii  663  nbn  694  ori  718  orci  726  olci  727  biorfi  741  imorri  744  dcbii  835  simp1i  1001  simp2i  1002  simp3i  1003  3mix1i  1164  3mix2i  1165  3mix3i  1166  3jaoi  1298  mptru  1357  dfnot  1366  mptnan  1418  mtpor  1420  mtpxor  1421  mpg  1444  19.23h  1491  hbequid  1506  axi12  1507  nfri  1512  spi  1529  19.21  1576  eximii  1595  19.35i  1618  nfn  1651  19.37aiv  1668  19.23  1671  exan  1686  equid  1694  hbae  1711  equvini  1751  equveli  1752  sbid  1767  sbieh  1783  exdistrfor  1793  dveeq2or  1809  ax11v  1820  ax11ev  1821  equs5or  1823  sb4or  1826  sb4bor  1828  nfsb2or  1830  sbequilem  1831  sbequi  1832  speiv  1855  nfsbxy  1935  nfsbxyt  1936  sbco  1961  sbcocom  1963  sbcomxyyz  1965  sbal1yz  1994  dvelimALT  2003  dvelimfv  2004  dvelimor  2011  eumoi  2052  moani  2089  elsb1  2148  elsb2  2149  eqeq1i  2178  eqeq2i  2181  eleq1i  2236  eleq2i  2237  nfcrii  2305  neeq1i  2355  neeq2i  2356  necon3i  2388  rspec  2522  rgen2a  2524  mprg  2527  r19.21  2546  r19.23  2578  raleqi  2669  rexeqi  2670  rabeqif  2721  elv  2734  elexi  2742  ceqsal  2759  vtocl3  2786  vtoclef  2803  vtocle  2804  spcv  2824  spcev  2825  clel3  2865  elabf  2873  elab2  2878  elab3  2882  euxfrdc  2916  reueq  2929  rmoimi2  2933  sbsbc  2959  sbc8g  2962  sbc6  2980  sbcie  2989  sbcrex  3034  csbvarg  3077  csbief  3093  csbie2  3098  sbnfc2  3109  sseli  3143  sselii  3144  sseq1i  3173  sseq2i  3174  difeq1i  3241  difeq2i  3242  uneq1i  3277  uneq2i  3278  ineq1i  3324  ineq2i  3325  ssinss1  3356  difdif2ss  3384  n0ii  3422  ne0ii  3423  vn0  3424  vn0m  3425  abf  3457  disj2  3469  difid  3482  0dif  3485  disjdif  3486  difin0  3487  undif1ss  3488  difdifdirss  3498  rgenm  3516  iftruei  3531  iffalsei  3534  ifbieq2i  3548  ifbieq12i  3550  pweqi  3568  pwid  3579  sneqi  3593  elsn  3597  elpr  3602  elsn2  3615  ralsn  3624  rexsn  3625  eltp  3629  rabrsndc  3649  preq1i  3661  preq2i  3662  prid1  3687  snnz  3700  snm  3701  prnz  3703  prm  3704  tpnz  3706  snsssn  3746  opeq1i  3766  opeq2i  3767  unieqi  3804  unissi  3817  inteqi  3833  intmin2  3855  intab  3858  intsn  3864  iinconstm  3880  iuniin  3881  iinss1  3883  iunxdif2  3919  ssiinf  3920  iinss  3922  iinss2  3923  iinab  3932  iundif2ss  3936  iindif2m  3938  iinin2m  3939  iunxsn  3947  iunxprg  3951  iinpw  3961  sndisj  3983  disjxsn  3985  breqi  3993  breq1i  3994  breq2i  3995  brab1  4034  opabbii  4054  truni  4099  bm1.3ii  4108  a9evsep  4109  ax9vsep  4110  zfnuleu  4111  axnul  4112  ssexi  4125  rabex  4131  elpw2  4141  pwnss  4143  iin0r  4153  intv  4154  pwex  4167  snex  4169  notnotsnex  4171  ord3ex  4174  dtruarb  4175  undifexmid  4177  intid  4207  opnzi  4218  copsexg  4227  opelopabf  4257  epelc  4274  elon  4357  inton  4376  onn0  4383  onm  4384  elsuc  4389  elsuc2  4390  sucid  4400  iunsuc  4403  onordi  4409  ontrci  4410  onelssi  4412  eusvnf  4436  ssonunii  4471  sucex  4481  onssi  4497  onsuci  4498  ordtriexmidlem  4501  ordtriexmidlem2  4502  ordtriexmid  4503  ontriexmidim  4504  ordtri2orexmid  4505  2ordpr  4506  ontr2exmid  4507  onsucsssucexmid  4509  onsucelsucexmid  4512  regexmidlemm  4514  reg2exmid  4518  onirri  4525  ruALT  4533  onprc  4534  sucon  4535  dtru  4542  0elsucexmid  4547  ordpwsucexmid  4552  ordtri2or2exmid  4553  ontri2orexmidim  4554  dcextest  4563  omex  4575  find  4581  omelon  4591  nnoni  4593  limom  4596  nnregexmid  4603  omsinds  4604  xpeq1i  4629  xpeq2i  4630  0nelxp  4637  opthprc  4660  mosubop  4675  releqi  4692  relssi  4700  relin1  4727  relin2  4728  reldif  4729  inopab  4741  difopab  4742  xpiindim  4746  opabbi2dv  4758  ideq  4761  coeq1i  4768  coeq2i  4769  cnveqi  4784  eldm  4806  eldm2  4807  dmeqi  4810  dmv  4825  rneqi  4837  elrnmpti  4862  dmex  4875  rnex  4876  reseq1i  4885  reseq2i  4886  residm  4921  resex  4930  resmpt3  4938  imaeq1i  4948  imaeq2i  4949  elima  4956  imaex  4964  elimasn  4976  args  4978  epini  4980  dfse2  4982  relbrcnv  4989  cotr  4990  issref  4991  cnvsym  4992  asymref  4994  intirr  4995  codir  4997  qfto  4998  ssrnres  5051  cnveq0  5065  cnvsn0  5077  dmsnop  5082  rnsnop  5089  resdm2  5099  dfco2a  5109  cocnvcnv1  5119  coi2  5125  coires1  5126  cnvssrndm  5130  cossxp  5131  cocnvres  5133  relrelss  5135  relcoi2  5139  unidmrn  5141  dfdm2  5143  unixpm  5144  cnvexg  5146  cnvex  5147  cnviinm  5150  iotaval  5169  funeqi  5217  funi  5228  funres  5237  funcnvsn  5241  funcnvcnv  5255  funin  5267  funcnvres  5269  isarep2  5283  fneq1i  5290  fneq2i  5291  fnresdisj  5306  fnresi  5313  mpt0  5323  dmmpti  5325  feq1i  5338  feq2i  5339  fdmi  5353  fun2  5369  fssres  5371  resasplitss  5375  fintm  5381  fconst6  5395  f1ores  5455  foimacnv  5458  resdif  5462  funcocnv2  5465  f1ovi  5479  fveq1i  5495  fveq2i  5497  0fv  5529  fvun1  5560  fvopab3ig  5568  fvmptss2  5569  mptrcl  5576  elfvmptrab1  5588  fndmdif  5599  fneqeql2  5603  f1oresrab  5659  fmptco  5660  fnressn  5680  fressnfv  5681  fmptap  5684  fvsnun1  5691  fvsnun2  5692  fsnunfv  5695  fconst2  5711  mptex  5720  riotabiia  5824  acexmidlema  5842  acexmidlemb  5843  acexmidlemcase  5846  acexmidlem2  5848  acexmidlemv  5849  oveq1i  5861  oveq2i  5862  oveqi  5864  oprabidlem  5882  0neqopab  5896  oprabbii  5906  oprabss  5937  mpompt  5943  funoprab  5951  fnoprab  5954  fovcl  5956  ovigg  5971  elmpocl  6045  resfunexgALT  6085  cofunexg  6086  mptexw  6090  opabex3d  6098  opabex3  6099  1st0  6121  2nd0  6122  op1st  6123  op2nd  6124  f1stres  6136  f2ndres  6137  fo1stresm  6138  fo2ndresm  6139  1stcof  6140  2ndcof  6141  1stexg  6144  2ndexg  6145  releldm2  6162  reldm  6163  dfoprab3  6168  mpomptsx  6174  mpompts  6175  fnmpoi  6181  dmmpo  6182  mpoexxg  6187  mpoexw  6190  1stconst  6198  2ndconst  6199  dfmpo  6200  algrflem  6206  algrflemg  6207  cnvoprab  6211  f1od2  6212  mpoxopn0yelv  6216  mpoxopoveq  6217  tposssxp  6226  brtpos2  6228  reldmtpos  6230  dftpos2  6238  dftpos4  6240  tpostpos  6241  tpostpos2  6242  tposfo  6248  tposf  6249  tposeqi  6254  tposex  6255  tposoprab  6257  issmo  6265  smores  6269  smores2  6271  iordsmo  6274  smo0  6275  tfrlem8  6295  tfrexlem  6311  tfr1onlem3  6315  tfr1onlemsucaccv  6318  tfr1onlembxssdm  6320  tfr1onlemres  6326  tfri1dALT  6328  tfri2  6343  rdgisuc1  6361  rdg0  6364  frecfun  6372  frec0g  6374  freccllem  6379  frecfcllem  6381  frecsuclem  6383  frecrdg  6385  2on0  6403  xp01disj  6410  2oconcl  6416  fnoa  6424  oaexg  6425  fnom  6427  omexg  6428  fnoei  6429  oeiexg  6430  oei0  6436  oacl  6437  oasuc  6441  o1p1e2  6445  omsuc  6449  nna0r  6455  nnm0r  6456  1onn  6497  2onn  6498  3onn  6499  4onn  6500  2ssom  6501  eqerlem  6542  elqs  6562  qsex  6568  ecqs  6573  iinerm  6583  th3qlem1  6613  th3q  6616  mapsn  6666  mapsnf1o3  6673  ixpiinm  6700  ixpssmap  6708  brdom  6726  f1dom  6736  enref  6741  dom2  6751  idssen  6753  ssdomg  6754  ensymi  6758  ensn1  6772  fiprc  6791  1domsn  6795  xpcomf1o  6801  xpcomco  6802  dom0  6814  0dom  6815  xpmapenlem  6825  phplem2  6829  php5  6834  snnen2og  6835  1nen2  6837  php5dom  6839  ssfilem  6851  ssfiexmid  6852  domfiexmid  6854  0fin  6860  diffitest  6863  findcard  6864  findcard2  6865  findcard2s  6866  isinfinf  6873  ac6sfi  6874  inffiexmid  6882  pw1fin  6886  unfiexmid  6893  xpfi  6905  fisseneq  6907  ssfirab  6909  en1eqsn  6923  snexxph  6925  sbthlem2  6933  sbthlemi3  6934  sbthlemi6  6937  sbthlem7  6938  fi0  6950  supeq1i  6963  infeq1i  6988  djuexb  7019  djuf1olemr  7029  inresflem  7035  djuinr  7038  updjudhcoinlf  7055  updjudhcoinrg  7056  casefun  7060  caserel  7062  caseinj  7064  caseinl  7066  caseinr  7067  omp1eomlem  7069  endjusym  7071  difinfsn  7075  difinfinf  7076  djuinj  7081  0ct  7082  ctmlemr  7083  ctssdclemn0  7085  ctssdccl  7086  omct  7092  ctfoex  7093  finomni  7114  exmidomni  7116  fodjuomni  7123  ctssexmid  7124  fodjumkv  7134  nninfwlporlem  7147  card0  7158  exmidonfinlem  7163  dju1p1e2  7167  exmidfodomrlemim  7171  exmidfodomrlemr  7172  exmidfodomrlemrALT  7173  3nelsucpw1  7204  sucpw1nss3  7205  3nsssucpw1  7206  0npi  7268  dmaddpi  7280  dmmulpi  7281  1lt2pi  7295  0nnq  7319  1nq  7321  dmaddpq  7334  dmmulpq  7335  rec1nq  7350  1lt2nq  7361  halfnqq  7365  prarloclemarch2  7374  enq0enq  7386  nqnq0pi  7393  nnnq0lem1  7401  addnnnq0  7404  mulnnnq0  7405  nq0m0r  7411  addpinq1  7419  prarloclem5  7455  prarloclemcalc  7457  1pr  7509  1idprl  7545  1idpru  7546  ltexprlemm  7555  recexprlem1ssl  7588  recexprlem1ssu  7589  suplocexprlemell  7668  suplocexprlem2b  7669  suplocexprlemmu  7673  suplocexprlemdisj  7675  suplocexprlemloc  7676  suplocexprlemub  7678  suplocexprlemlub  7679  prsrlem1  7697  addsrpr  7700  mulsrpr  7701  gt0srpr  7703  0nsr  7704  0r  7705  1sr  7706  m1r  7707  m1m1sr  7716  caucvgsr  7757  suplocsrlempr  7762  addresr  7792  mulresr  7793  pitonnlem1  7800  peano1nnnn  7807  axi2m1  7830  axcnre  7836  peano5nnnn  7847  axcaucvg  7855  mulid1i  7915  mulid2i  7916  pnfnre  7954  mnfnre  7955  pnfnemnf  7967  mnfxr  7969  rexri  7970  ltnri  8005  ltleii  8015  00id  8053  addid1i  8054  addid2i  8055  0cnALT  8102  negeqi  8106  negicn  8113  neg0  8158  renegcli  8174  negcli  8180  negidi  8181  negnegi  8182  subidi  8183  subid1i  8184  negne0bi  8185  negrebi  8186  mul02i  8302  mul01i  8303  mulm1i  8315  leidi  8397  gt0ne0ii  8399  inelr  8496  msqge0i  8529  gt0ap0ii  8540  1div1e1  8614  div1i  8650  eqnegi  8651  recclapi  8652  recidapi  8653  divmulapi  8676  rerecclapi  8687  redivclapi  8689  recgt0  8759  ltp1i  8814  divgt0ii  8828  ltmul1ii  8837  ltdiv1ii  8838  sup3exmid  8866  peano5nni  8874  nnrei  8880  1nn  8882  nngt0i  8901  neg1ap0  8980  2timesi  9001  times2i  9002  2nn  9032  3nn  9033  4nn  9034  5nn  9035  6nn  9036  7nn  9037  8nn  9038  9nn  9039  2muline0  9096  rehalfcli  9119  nn0ssre  9132  nnnn0i  9136  dfn2  9141  0nn0  9143  nn0ge0i  9155  zrei  9211  neg1z  9237  nn0negzi  9240  dfz2  9277  nneoi  9309  peano5uzi  9314  dfuzi  9315  nn0ind-raph  9322  deceq1i  9342  deceq2i  9343  10nn  9351  numltc  9361  eluzel2  9485  eluz1i  9487  nn0uz  9514  nnuz  9515  infrenegsupex  9546  lbzbi  9568  divfnzn  9573  qdivcl  9595  irrmul  9599  cnref1o  9602  0ltpnf  9732  mnflt0  9734  0lepnf  9740  xrltnsym  9743  xrlttri3  9747  nltpnft  9764  ngtmnft  9767  xrrebnd  9769  xnegmnf  9779  xneg0  9781  xltnegi  9785  xaddmnf1  9798  xaddmnf2  9799  mnfaddpnf  9801  xaddid1  9812  xnn0lenn0nn0  9815  xnn0xadd0  9817  xposdif  9832  ixxex  9849  iooval2  9865  unirnioo  9923  ioorebasg  9925  elrege0  9926  fzval2  9961  fzen  9992  fzprval  10031  fztpval  10032  uzdisj  10042  ige2m1fz  10059  fz01or  10060  fz1ssfz0  10066  fz0sn  10070  fz0tp  10071  fz0to3un2pr  10072  fz0to4untppr  10073  nn0disj  10087  1fv  10088  4fvwrd4  10089  fzo0ss1  10123  fzo01  10165  fzo12sn  10166  fzo0to2pr  10167  fzo0to3tp  10168  fzo0to42pr  10169  qbtwnxr  10207  flval  10221  modqfrac  10286  modqmulnn  10291  q2txmodxeq0  10333  frecuzrdgdom  10367  frecuzrdgfun  10369  frecuzrdgsuct  10373  frechashgf1o  10377  nnct  10384  fxnn0nninf  10387  0tonninf  10388  1tonninf  10389  iseqvalcbv  10406  ser0f  10464  0exp0e1  10474  qexpcl  10485  qexpclz  10490  m1expcl2  10491  1exp  10498  sqvali  10548  sqcli  10549  sqeq0i  10550  resqcli  10553  sq1  10562  neg1sqe1  10563  iexpcyc  10573  qsqeqor  10579  facnn  10654  fac0  10655  fac1  10656  fac2  10658  fac3  10659  fac4  10660  bcval  10676  bcm1k  10687  bcpasc  10693  bccl  10694  4bc3eq4  10700  4bc2eq6  10701  hashinfom  10705  hashennn  10707  hashfz1  10710  fihasheq0  10721  hash0  10724  hashsng  10726  fihashen1  10727  omgadd  10730  hashp1i  10738  hashxp  10754  fimaxq  10755  zfz1iso  10769  shftidt2  10789  cjexp  10850  re0  10852  im0  10853  re1  10854  im1  10855  cj0  10858  cji  10859  recli  10868  imcli  10869  cjcli  10870  replimi  10871  cjcji  10872  reim0bi  10873  rerebi  10874  cjrebi  10875  recji  10876  imcji  10877  cjmulrcli  10878  cjmulvali  10879  cjmulge0i  10880  renegi  10881  imnegi  10882  cjnegi  10883  addcji  10884  uzin2  10944  rexanuz  10945  rexfiuz  10946  sqrtrval  10957  sqrt0  10961  resqrexlemcalc3  10973  resqrexlemcvg  10976  resqrex  10983  abs0  11015  absi  11016  qabsor  11032  absimle  11041  recan  11066  caubnd2  11074  leabsi  11085  absrei  11086  sqrtpclii  11087  sqrtgt0ii  11088  absvalsqi  11097  absvalsq2i  11098  abscli  11099  absge0i  11100  absval2i  11101  abs00i  11102  absgt0api  11103  absnegi  11104  abscji  11105  releabsi  11106  infxrnegsupex  11219  xrbdtri  11232  cbvsum  11316  sumeq1i  11319  sum0  11344  isumz  11345  fisumss  11348  fsumsersdc  11351  fsumadd  11362  isumclim  11377  isumclim3  11379  fsumcnv  11393  modfsummodlem1  11412  fsumrelem  11427  binomlem  11439  binom  11440  arisum2  11455  expcnv  11460  0.999...  11477  prodf1f  11499  cbvprod  11514  prodeq1i  11517  zproddc  11535  zprodap0  11537  prod0  11541  fprodssdc  11546  prodsnf  11548  fprodcnv  11581  fprodge0  11593  fprodge1  11595  ef0lem  11616  esum  11618  ere  11626  ege2le3  11627  ef0  11628  eff2  11636  efsep  11647  reeff1  11656  sin0  11685  cos0  11686  ef01bndlem  11712  cos2bnd  11716  sincos1sgn  11720  sincos2sgn  11721  sin4lt0  11722  eirr  11734  0dvds  11766  dvds1  11806  z0even  11863  n2dvdsm1  11865  z2even  11866  n2dvds3  11867  ndvdssub  11882  ndvdsi  11885  flodddiv4  11886  zsupssdc  11902  gcddvds  11911  gcd1  11935  6gcd4e2  11943  bezoutlembi  11953  dfgcd3  11958  dfgcd2  11962  lcmval  12010  lcmcllem  12014  lcmledvds  12017  3lcm2e6woprm  12033  qredeu  12044  isprm2lem  12063  isprm3  12065  prm2orodd  12073  isprm5lem  12088  sqrt2irr0  12111  pw2dvds  12113  phicl2  12161  phi1  12166  dfphi2  12167  phiprmpw  12169  eulerthlemrprm  12176  eulerthlemh  12178  odzval  12188  oddprm  12206  pczpre  12244  pcdiv  12249  pc0  12251  pcqdiv  12254  pcrec  12255  pcexp  12256  pcxcl  12258  pcdvdstr  12273  pc2dvds  12276  dvdsprmpweqnn  12282  pcmpt  12288  qexpz  12297  pockthi  12303  1arith2  12313  ennnfonelemp1  12354  ennnfonelem1  12355  ennnfonelemkh  12360  ennnfonelemex  12362  ennnfonelemnn0  12370  ennnfonelemr  12371  exmidunben  12374  ctinfomlemom  12375  ctinfom  12376  ctinf  12378  qnnen  12379  omctfn  12391  omiunct  12392  ssnnctlemct  12394  nninfdc  12401  structcnvcnv  12425  structfun  12427  structfn  12428  ndxarg  12432  ndxid  12433  setsresg  12447  setsslnid  12460  basmex  12467  basmexd  12468  strleun  12500  strle1g  12501  ismgmn0  12605  fn0g  12622  0g0  12623  istopon  12770  topontopi  12773  toponunii  12774  toponrestid  12778  istps  12789  topontopn  12794  eltpsi  12798  eltg4i  12814  eltg3  12816  tg1  12818  tg2  12819  tgclb  12824  topnex  12845  sn0topon  12847  distps  12850  cldrcl  12861  sn0cld  12896  restco  12933  lmrcl  12950  ssidcn  12969  cnconst2  12992  cnptopresti  12997  cnptoprest  12998  txuni2  13015  txbas  13017  eltx  13018  txcnp  13030  upxp  13031  txcnmpt  13032  uptx  13033  txcn  13034  txrest  13035  txlm  13038  cnmptid  13040  cnmpt1st  13047  cnmpt2nd  13048  hmeofn  13061  psmetge0  13090  ismeti  13105  xmetunirn  13117  xmetge0  13124  unirnblps  13181  unirnbl  13182  mopnex  13264  qtopbasss  13280  retop  13283  uniretop  13284  iooretopg  13287  cnxmet  13290  cntoptopon  13291  cnbl0  13293  rexmet  13300  blssioo  13304  tgioo  13305  tgqioo  13306  cnopnap  13353  limcresi  13394  dvfvalap  13409  dvidlemap  13419  dvcnp2cntop  13422  dvcoapbr  13430  dvexp2  13435  dvrecap  13436  dveflem  13446  dvef  13447  reeff1o  13453  sin0pilem1  13461  sin0pilem2  13462  pilem3  13463  pigt2lt4  13464  pire  13466  sinhalfpilem  13471  pidiv2halves  13475  cosneghalfpi  13478  cospi  13480  efipi  13481  sin2pi  13483  cos2pi  13484  ef2pi  13485  cosq14gt0  13512  coseq00topi  13515  coseq0negpitopi  13516  sincos4thpi  13520  sincos6thpi  13522  sincos3rdpi  13523  pigt3  13524  cos02pilt1  13531  ioocosf1o  13534  dfrelog  13540  relogf1o  13541  relogcl  13542  relogiso  13553  rpcxpsqrt  13601  rpabscxpbnd  13618  2logb9irr  13648  2logb9irrALT  13651  sqrt2cxp2logb9e3  13652  2irrexpq  13653  2logb9irrap  13654  2irrexpqap  13655  lgsdir2lem1  13688  lgsdir2lem2  13689  lgsdir2lem4  13691  lgsdir2lem5  13692  lgsdi  13697  2sqlem9  13719  2sqlem10  13720  ex-fl  13725  ex-ceil  13726  ex-exp  13727  ex-fac  13728  ex-gcd  13731  bj-stfal  13742  bj-stst  13745  bj-dcfal  13755  bj-dcdc  13759  bj-stdc  13760  bj-dcst  13761  bj-el2oss1o  13774  elabf2  13782  bd0  13824  bdeli  13846  bdcriota  13883  bdbm1.3ii  13891  bdinex1  13899  bdssexi  13903  bj-inex  13907  bj-snex  13913  bj-sucex  13923  bj-d0clsepcl  13925  bj-omind  13934  bj-om  13937  bj-2inf  13938  bj-peano2  13939  bdpeano5  13943  bj-omssonALT  13963  bj-inf2vnlem1  13970  bj-omex2  13977  bj-nn0sucALT  13978  012of  13993  2o01f  13994  subctctexmid  13999  nninfall  14007  nninfsellemqall  14013  nninfsellemeqinf  14014  nninfomnilem  14016  nninfomni  14017  exmidsbthrlem  14019  sbthom  14023  isomninnlem  14027  isomninn  14028  cvgcmp2nlemabs  14029  iooreen  14032  trilpolemisumle  14035  trilpolemeq1  14037  trilpo  14040  trirec0  14041  apdifflemr  14044  iswomninnlem  14046  iswomninn  14047  ismkvnnlem  14049  ismkvnn  14050  redcwlpo  14052  dcapnconst  14057  nconstwlpolem0  14059  nconstwlpo  14062  neapmkv  14064  taupi  14067