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

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  423  pm2.65i  629  notnoti  635  pm2.21i  636  pm2.24ii  637  notbii  658  nbn  689  ori  713  orci  721  olci  722  biorfi  736  imorri  739  dcbii  830  simp1i  996  simp2i  997  simp3i  998  3mix1i  1159  3mix2i  1160  3mix3i  1161  3jaoi  1293  mptru  1352  dfnot  1361  mptnan  1413  mtpor  1415  mtpxor  1416  mpg  1439  19.23h  1486  hbequid  1501  axi12  1502  nfri  1507  spi  1524  19.21  1571  eximii  1590  19.35i  1613  nfn  1646  19.37aiv  1663  19.23  1666  exan  1681  equid  1689  hbae  1706  equvini  1746  equveli  1747  sbid  1762  sbieh  1778  exdistrfor  1788  dveeq2or  1804  ax11v  1815  ax11ev  1816  equs5or  1818  sb4or  1821  sb4bor  1823  nfsb2or  1825  sbequilem  1826  sbequi  1827  speiv  1850  nfsbxy  1930  nfsbxyt  1931  sbco  1956  sbcocom  1958  sbcomxyyz  1960  sbal1yz  1989  dvelimALT  1998  dvelimfv  1999  dvelimor  2006  eumoi  2047  moani  2084  elsb1  2143  elsb2  2144  eqeq1i  2173  eqeq2i  2176  eleq1i  2232  eleq2i  2233  nfcrii  2301  neeq1i  2351  neeq2i  2352  necon3i  2384  rspec  2518  rgen2a  2520  mprg  2523  r19.21  2542  r19.23  2574  raleqi  2665  rexeqi  2666  rabeqif  2717  elv  2730  elexi  2738  ceqsal  2755  vtocl3  2782  vtoclef  2799  vtocle  2800  spcv  2820  spcev  2821  clel3  2861  elabf  2869  elab2  2874  elab3  2878  euxfrdc  2912  reueq  2925  rmoimi2  2929  sbsbc  2955  sbc8g  2958  sbc6  2976  sbcie  2985  sbcrex  3030  csbvarg  3073  csbief  3089  csbie2  3094  sbnfc2  3105  sseli  3138  sselii  3139  sseq1i  3168  sseq2i  3169  difeq1i  3236  difeq2i  3237  uneq1i  3272  uneq2i  3273  ineq1i  3319  ineq2i  3320  ssinss1  3351  difdif2ss  3379  n0ii  3417  ne0ii  3418  vn0  3419  vn0m  3420  abf  3452  disj2  3464  difid  3477  0dif  3480  disjdif  3481  difin0  3482  undif1ss  3483  difdifdirss  3493  rgenm  3511  iftruei  3526  iffalsei  3529  ifbieq2i  3543  ifbieq12i  3545  pweqi  3563  pwid  3574  sneqi  3588  elsn  3592  elpr  3597  elsn2  3610  ralsn  3619  rexsn  3620  eltp  3624  rabrsndc  3644  preq1i  3656  preq2i  3657  prid1  3682  snnz  3695  snm  3696  prnz  3698  prm  3699  tpnz  3701  snsssn  3741  opeq1i  3761  opeq2i  3762  unieqi  3799  unissi  3812  inteqi  3828  intmin2  3850  intab  3853  intsn  3859  iinconstm  3875  iuniin  3876  iinss1  3878  iunxdif2  3914  ssiinf  3915  iinss  3917  iinss2  3918  iinab  3927  iundif2ss  3931  iindif2m  3933  iinin2m  3934  iunxsn  3942  iunxprg  3946  iinpw  3956  sndisj  3978  disjxsn  3980  breqi  3988  breq1i  3989  breq2i  3990  brab1  4029  opabbii  4049  truni  4094  bm1.3ii  4103  a9evsep  4104  ax9vsep  4105  zfnuleu  4106  axnul  4107  ssexi  4120  rabex  4126  elpw2  4136  pwnss  4138  iin0r  4148  intv  4149  pwex  4162  snex  4164  notnotsnex  4166  ord3ex  4169  dtruarb  4170  undifexmid  4172  intid  4202  opnzi  4213  copsexg  4222  opelopabf  4252  epelc  4269  elon  4352  inton  4371  onn0  4378  onm  4379  elsuc  4384  elsuc2  4385  sucid  4395  iunsuc  4398  onordi  4404  ontrci  4405  onelssi  4407  eusvnf  4431  ssonunii  4466  sucex  4476  onssi  4492  onsuci  4493  ordtriexmidlem  4496  ordtriexmidlem2  4497  ordtriexmid  4498  ontriexmidim  4499  ordtri2orexmid  4500  2ordpr  4501  ontr2exmid  4502  onsucsssucexmid  4504  onsucelsucexmid  4507  regexmidlemm  4509  reg2exmid  4513  onirri  4520  ruALT  4528  onprc  4529  sucon  4530  dtru  4537  0elsucexmid  4542  ordpwsucexmid  4547  ordtri2or2exmid  4548  ontri2orexmidim  4549  dcextest  4558  omex  4570  find  4576  omelon  4586  nnoni  4588  limom  4591  nnregexmid  4598  omsinds  4599  xpeq1i  4624  xpeq2i  4625  0nelxp  4632  opthprc  4655  mosubop  4670  releqi  4687  relssi  4695  relin1  4722  relin2  4723  reldif  4724  inopab  4736  difopab  4737  xpiindim  4741  opabbi2dv  4753  ideq  4756  coeq1i  4763  coeq2i  4764  cnveqi  4779  eldm  4801  eldm2  4802  dmeqi  4805  dmv  4820  rneqi  4832  elrnmpti  4857  dmex  4870  rnex  4871  reseq1i  4880  reseq2i  4881  residm  4916  resex  4925  resmpt3  4933  imaeq1i  4943  imaeq2i  4944  elima  4951  imaex  4959  elimasn  4971  args  4973  epini  4975  dfse2  4977  relbrcnv  4984  cotr  4985  issref  4986  cnvsym  4987  asymref  4989  intirr  4990  codir  4992  qfto  4993  ssrnres  5046  cnveq0  5060  cnvsn0  5072  dmsnop  5077  rnsnop  5084  resdm2  5094  dfco2a  5104  cocnvcnv1  5114  coi2  5120  coires1  5121  cnvssrndm  5125  cossxp  5126  cocnvres  5128  relrelss  5130  relcoi2  5134  unidmrn  5136  dfdm2  5138  unixpm  5139  cnvexg  5141  cnvex  5142  cnviinm  5145  iotaval  5164  funeqi  5209  funi  5220  funres  5229  funcnvsn  5233  funcnvcnv  5247  funin  5259  funcnvres  5261  isarep2  5275  fneq1i  5282  fneq2i  5283  fnresdisj  5298  fnresi  5305  mpt0  5315  dmmpti  5317  feq1i  5330  feq2i  5331  fdmi  5345  fun2  5361  fssres  5363  resasplitss  5367  fintm  5373  fconst6  5387  f1ores  5447  foimacnv  5450  resdif  5454  funcocnv2  5457  f1ovi  5471  fveq1i  5487  fveq2i  5489  0fv  5521  fvun1  5552  fvopab3ig  5560  fvmptss2  5561  mptrcl  5568  elfvmptrab1  5580  fndmdif  5590  fneqeql2  5594  f1oresrab  5650  fmptco  5651  fnressn  5671  fressnfv  5672  fmptap  5675  fvsnun1  5682  fvsnun2  5683  fsnunfv  5686  fconst2  5702  mptex  5711  riotabiia  5815  acexmidlema  5833  acexmidlemb  5834  acexmidlemcase  5837  acexmidlem2  5839  acexmidlemv  5840  oveq1i  5852  oveq2i  5853  oveqi  5855  oprabidlem  5873  0neqopab  5887  oprabbii  5897  oprabss  5928  mpompt  5934  funoprab  5942  fnoprab  5945  fovcl  5947  ovigg  5962  elmpocl  6036  resfunexgALT  6076  cofunexg  6077  mptexw  6081  opabex3d  6089  opabex3  6090  1st0  6112  2nd0  6113  op1st  6114  op2nd  6115  f1stres  6127  f2ndres  6128  fo1stresm  6129  fo2ndresm  6130  1stcof  6131  2ndcof  6132  1stexg  6135  2ndexg  6136  releldm2  6153  reldm  6154  dfoprab3  6159  mpomptsx  6165  mpompts  6166  fnmpoi  6172  dmmpo  6173  mpoexxg  6178  mpoexw  6181  1stconst  6189  2ndconst  6190  dfmpo  6191  algrflem  6197  algrflemg  6198  cnvoprab  6202  f1od2  6203  mpoxopn0yelv  6207  mpoxopoveq  6208  tposssxp  6217  brtpos2  6219  reldmtpos  6221  dftpos2  6229  dftpos4  6231  tpostpos  6232  tpostpos2  6233  tposfo  6239  tposf  6240  tposeqi  6245  tposex  6246  tposoprab  6248  issmo  6256  smores  6260  smores2  6262  iordsmo  6265  smo0  6266  tfrlem8  6286  tfrexlem  6302  tfr1onlem3  6306  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfr1onlemres  6317  tfri1dALT  6319  tfri2  6334  rdgisuc1  6352  rdg0  6355  frecfun  6363  frec0g  6365  freccllem  6370  frecfcllem  6372  frecsuclem  6374  frecrdg  6376  2on0  6394  xp01disj  6401  2oconcl  6407  fnoa  6415  oaexg  6416  fnom  6418  omexg  6419  fnoei  6420  oeiexg  6421  oei0  6427  oacl  6428  oasuc  6432  o1p1e2  6436  omsuc  6440  nna0r  6446  nnm0r  6447  1onn  6488  2onn  6489  3onn  6490  4onn  6491  eqerlem  6532  elqs  6552  qsex  6558  ecqs  6563  iinerm  6573  th3qlem1  6603  th3q  6606  mapsn  6656  mapsnf1o3  6663  ixpiinm  6690  ixpssmap  6698  brdom  6716  f1dom  6726  enref  6731  dom2  6741  idssen  6743  ssdomg  6744  ensymi  6748  ensn1  6762  fiprc  6781  1domsn  6785  xpcomf1o  6791  xpcomco  6792  dom0  6804  0dom  6805  xpmapenlem  6815  phplem2  6819  php5  6824  snnen2og  6825  1nen2  6827  php5dom  6829  ssfilem  6841  ssfiexmid  6842  domfiexmid  6844  0fin  6850  diffitest  6853  findcard  6854  findcard2  6855  findcard2s  6856  isinfinf  6863  ac6sfi  6864  inffiexmid  6872  pw1fin  6876  unfiexmid  6883  xpfi  6895  fisseneq  6897  ssfirab  6899  en1eqsn  6913  snexxph  6915  sbthlem2  6923  sbthlemi3  6924  sbthlemi6  6927  sbthlem7  6928  fi0  6940  supeq1i  6953  infeq1i  6978  djuexb  7009  djuf1olemr  7019  inresflem  7025  djuinr  7028  updjudhcoinlf  7045  updjudhcoinrg  7046  casefun  7050  caserel  7052  caseinj  7054  caseinl  7056  caseinr  7057  omp1eomlem  7059  endjusym  7061  difinfsn  7065  difinfinf  7066  djuinj  7071  0ct  7072  ctmlemr  7073  ctssdclemn0  7075  ctssdccl  7076  omct  7082  ctfoex  7083  finomni  7104  exmidomni  7106  fodjuomni  7113  ctssexmid  7114  fodjumkv  7124  card0  7144  exmidonfinlem  7149  dju1p1e2  7153  exmidfodomrlemim  7157  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  3nelsucpw1  7190  sucpw1nss3  7191  3nsssucpw1  7192  0npi  7254  dmaddpi  7266  dmmulpi  7267  1lt2pi  7281  0nnq  7305  1nq  7307  dmaddpq  7320  dmmulpq  7321  rec1nq  7336  1lt2nq  7347  halfnqq  7351  prarloclemarch2  7360  enq0enq  7372  nqnq0pi  7379  nnnq0lem1  7387  addnnnq0  7390  mulnnnq0  7391  nq0m0r  7397  addpinq1  7405  prarloclem5  7441  prarloclemcalc  7443  1pr  7495  1idprl  7531  1idpru  7532  ltexprlemm  7541  recexprlem1ssl  7574  recexprlem1ssu  7575  suplocexprlemell  7654  suplocexprlem2b  7655  suplocexprlemmu  7659  suplocexprlemdisj  7661  suplocexprlemloc  7662  suplocexprlemub  7664  suplocexprlemlub  7665  prsrlem1  7683  addsrpr  7686  mulsrpr  7687  gt0srpr  7689  0nsr  7690  0r  7691  1sr  7692  m1r  7693  m1m1sr  7702  caucvgsr  7743  suplocsrlempr  7748  addresr  7778  mulresr  7779  pitonnlem1  7786  peano1nnnn  7793  axi2m1  7816  axcnre  7822  peano5nnnn  7833  axcaucvg  7841  mulid1i  7901  mulid2i  7902  pnfnre  7940  mnfnre  7941  pnfnemnf  7953  mnfxr  7955  rexri  7956  ltnri  7991  ltleii  8001  00id  8039  addid1i  8040  addid2i  8041  0cnALT  8088  negeqi  8092  negicn  8099  neg0  8144  renegcli  8160  negcli  8166  negidi  8167  negnegi  8168  subidi  8169  subid1i  8170  negne0bi  8171  negrebi  8172  mul02i  8288  mul01i  8289  mulm1i  8301  leidi  8383  gt0ne0ii  8385  inelr  8482  msqge0i  8515  gt0ap0ii  8526  1div1e1  8600  div1i  8636  eqnegi  8637  recclapi  8638  recidapi  8639  divmulapi  8662  rerecclapi  8673  redivclapi  8675  recgt0  8745  ltp1i  8800  divgt0ii  8814  ltmul1ii  8823  ltdiv1ii  8824  sup3exmid  8852  peano5nni  8860  nnrei  8866  1nn  8868  nngt0i  8887  neg1ap0  8966  2timesi  8987  times2i  8988  2nn  9018  3nn  9019  4nn  9020  5nn  9021  6nn  9022  7nn  9023  8nn  9024  9nn  9025  2muline0  9082  rehalfcli  9105  nn0ssre  9118  nnnn0i  9122  dfn2  9127  0nn0  9129  nn0ge0i  9141  zrei  9197  neg1z  9223  nn0negzi  9226  dfz2  9263  nneoi  9295  peano5uzi  9300  dfuzi  9301  nn0ind-raph  9308  deceq1i  9328  deceq2i  9329  10nn  9337  numltc  9347  eluzel2  9471  eluz1i  9473  nn0uz  9500  nnuz  9501  infrenegsupex  9532  lbzbi  9554  divfnzn  9559  qdivcl  9581  irrmul  9585  cnref1o  9588  0ltpnf  9718  mnflt0  9720  0lepnf  9726  xrltnsym  9729  xrlttri3  9733  nltpnft  9750  ngtmnft  9753  xrrebnd  9755  xnegmnf  9765  xneg0  9767  xltnegi  9771  xaddmnf1  9784  xaddmnf2  9785  mnfaddpnf  9787  xaddid1  9798  xnn0lenn0nn0  9801  xnn0xadd0  9803  xposdif  9818  ixxex  9835  iooval2  9851  unirnioo  9909  ioorebasg  9911  elrege0  9912  fzval2  9947  fzen  9978  fzprval  10017  fztpval  10018  uzdisj  10028  ige2m1fz  10045  fz01or  10046  fz1ssfz0  10052  fz0sn  10056  fz0tp  10057  fz0to3un2pr  10058  fz0to4untppr  10059  nn0disj  10073  1fv  10074  4fvwrd4  10075  fzo0ss1  10109  fzo01  10151  fzo12sn  10152  fzo0to2pr  10153  fzo0to3tp  10154  fzo0to42pr  10155  qbtwnxr  10193  flval  10207  modqfrac  10272  modqmulnn  10277  q2txmodxeq0  10319  frecuzrdgdom  10353  frecuzrdgfun  10355  frecuzrdgsuct  10359  frechashgf1o  10363  nnct  10370  fxnn0nninf  10373  0tonninf  10374  1tonninf  10375  iseqvalcbv  10392  ser0f  10450  0exp0e1  10460  qexpcl  10471  qexpclz  10476  m1expcl2  10477  1exp  10484  sqvali  10534  sqcli  10535  sqeq0i  10536  resqcli  10539  sq1  10548  neg1sqe1  10549  iexpcyc  10559  qsqeqor  10565  facnn  10640  fac0  10641  fac1  10642  fac2  10644  fac3  10645  fac4  10646  bcval  10662  bcm1k  10673  bcpasc  10679  bccl  10680  4bc3eq4  10686  4bc2eq6  10687  hashinfom  10691  hashennn  10693  hashfz1  10696  fihasheq0  10707  hash0  10710  hashsng  10711  fihashen1  10712  omgadd  10715  hashp1i  10723  hashxp  10739  fimaxq  10740  zfz1iso  10754  shftidt2  10774  cjexp  10835  re0  10837  im0  10838  re1  10839  im1  10840  cj0  10843  cji  10844  recli  10853  imcli  10854  cjcli  10855  replimi  10856  cjcji  10857  reim0bi  10858  rerebi  10859  cjrebi  10860  recji  10861  imcji  10862  cjmulrcli  10863  cjmulvali  10864  cjmulge0i  10865  renegi  10866  imnegi  10867  cjnegi  10868  addcji  10869  uzin2  10929  rexanuz  10930  rexfiuz  10931  sqrtrval  10942  sqrt0  10946  resqrexlemcalc3  10958  resqrexlemcvg  10961  resqrex  10968  abs0  11000  absi  11001  qabsor  11017  absimle  11026  recan  11051  caubnd2  11059  leabsi  11070  absrei  11071  sqrtpclii  11072  sqrtgt0ii  11073  absvalsqi  11082  absvalsq2i  11083  abscli  11084  absge0i  11085  absval2i  11086  abs00i  11087  absgt0api  11088  absnegi  11089  abscji  11090  releabsi  11091  infxrnegsupex  11204  xrbdtri  11217  cbvsum  11301  sumeq1i  11304  sum0  11329  isumz  11330  fisumss  11333  fsumsersdc  11336  fsumadd  11347  isumclim  11362  isumclim3  11364  fsumcnv  11378  modfsummodlem1  11397  fsumrelem  11412  binomlem  11424  binom  11425  arisum2  11440  expcnv  11445  0.999...  11462  prodf1f  11484  cbvprod  11499  prodeq1i  11502  zproddc  11520  zprodap0  11522  prod0  11526  fprodssdc  11531  prodsnf  11533  fprodcnv  11566  fprodge0  11578  fprodge1  11580  ef0lem  11601  esum  11603  ere  11611  ege2le3  11612  ef0  11613  eff2  11621  efsep  11632  reeff1  11641  sin0  11670  cos0  11671  ef01bndlem  11697  cos2bnd  11701  sincos1sgn  11705  sincos2sgn  11706  sin4lt0  11707  eirr  11719  0dvds  11751  dvds1  11791  z0even  11848  n2dvdsm1  11850  z2even  11851  n2dvds3  11852  ndvdssub  11867  ndvdsi  11870  flodddiv4  11871  zsupssdc  11887  gcddvds  11896  gcd1  11920  6gcd4e2  11928  bezoutlembi  11938  dfgcd3  11943  dfgcd2  11947  lcmval  11995  lcmcllem  11999  lcmledvds  12002  3lcm2e6woprm  12018  qredeu  12029  isprm2lem  12048  isprm3  12050  prm2orodd  12058  isprm5lem  12073  sqrt2irr0  12096  pw2dvds  12098  phicl2  12146  phi1  12151  dfphi2  12152  phiprmpw  12154  eulerthlemrprm  12161  eulerthlemh  12163  odzval  12173  oddprm  12191  pczpre  12229  pcdiv  12234  pc0  12236  pcqdiv  12239  pcrec  12240  pcexp  12241  pcxcl  12243  pcdvdstr  12258  pc2dvds  12261  dvdsprmpweqnn  12267  pcmpt  12273  qexpz  12282  pockthi  12288  1arith2  12298  ennnfonelemp1  12339  ennnfonelem1  12340  ennnfonelemkh  12345  ennnfonelemex  12347  ennnfonelemnn0  12355  ennnfonelemr  12356  exmidunben  12359  ctinfomlemom  12360  ctinfom  12361  ctinf  12363  qnnen  12364  omctfn  12376  omiunct  12377  ssnnctlemct  12379  nninfdc  12386  structcnvcnv  12410  structfun  12412  structfn  12413  ndxarg  12417  ndxid  12418  setsresg  12432  setsslnid  12445  basmex  12452  strleun  12484  strle1g  12485  ismgmn0  12589  fn0g  12606  0g0  12607  istopon  12651  topontopi  12654  toponunii  12655  toponrestid  12659  istps  12670  topontopn  12675  eltpsi  12679  eltg4i  12695  eltg3  12697  tg1  12699  tg2  12700  tgclb  12705  topnex  12726  sn0topon  12728  distps  12731  cldrcl  12742  sn0cld  12777  restco  12814  lmrcl  12831  ssidcn  12850  cnconst2  12873  cnptopresti  12878  cnptoprest  12879  txuni2  12896  txbas  12898  eltx  12899  txcnp  12911  upxp  12912  txcnmpt  12913  uptx  12914  txcn  12915  txrest  12916  txlm  12919  cnmptid  12921  cnmpt1st  12928  cnmpt2nd  12929  hmeofn  12942  psmetge0  12971  ismeti  12986  xmetunirn  12998  xmetge0  13005  unirnblps  13062  unirnbl  13063  mopnex  13145  qtopbasss  13161  retop  13164  uniretop  13165  iooretopg  13168  cnxmet  13171  cntoptopon  13172  cnbl0  13174  rexmet  13181  blssioo  13185  tgioo  13186  tgqioo  13187  cnopnap  13234  limcresi  13275  dvfvalap  13290  dvidlemap  13300  dvcnp2cntop  13303  dvcoapbr  13311  dvexp2  13316  dvrecap  13317  dveflem  13327  dvef  13328  reeff1o  13334  sin0pilem1  13342  sin0pilem2  13343  pilem3  13344  pigt2lt4  13345  pire  13347  sinhalfpilem  13352  pidiv2halves  13356  cosneghalfpi  13359  cospi  13361  efipi  13362  sin2pi  13364  cos2pi  13365  ef2pi  13366  cosq14gt0  13393  coseq00topi  13396  coseq0negpitopi  13397  sincos4thpi  13401  sincos6thpi  13403  sincos3rdpi  13404  pigt3  13405  cos02pilt1  13412  ioocosf1o  13415  dfrelog  13421  relogf1o  13422  relogcl  13423  relogiso  13434  rpcxpsqrt  13482  rpabscxpbnd  13499  2logb9irr  13529  2logb9irrALT  13532  sqrt2cxp2logb9e3  13533  2irrexpq  13534  2logb9irrap  13535  2irrexpqap  13536  lgsdir2lem1  13569  lgsdir2lem2  13570  lgsdir2lem4  13572  lgsdir2lem5  13573  lgsdi  13578  2sqlem9  13600  2sqlem10  13601  ex-fl  13606  ex-ceil  13607  ex-exp  13608  ex-fac  13609  ex-gcd  13612  bj-stfal  13623  bj-stst  13626  bj-dcfal  13636  bj-dcdc  13640  bj-stdc  13641  bj-dcst  13642  bj-el2oss1o  13655  elabf2  13663  2ssom  13684  bd0  13706  bdeli  13728  bdcriota  13765  bdbm1.3ii  13773  bdinex1  13781  bdssexi  13785  bj-inex  13789  bj-snex  13795  bj-sucex  13805  bj-d0clsepcl  13807  bj-omind  13816  bj-om  13819  bj-2inf  13820  bj-peano2  13821  bdpeano5  13825  bj-omssonALT  13845  bj-inf2vnlem1  13852  bj-omex2  13859  bj-nn0sucALT  13860  012of  13875  2o01f  13876  subctctexmid  13881  nninfall  13889  nninfsellemqall  13895  nninfsellemeqinf  13896  nninfomnilem  13898  nninfomni  13899  exmidsbthrlem  13901  sbthom  13905  isomninnlem  13909  isomninn  13910  cvgcmp2nlemabs  13911  iooreen  13914  trilpolemisumle  13917  trilpolemeq1  13919  trilpo  13922  trirec0  13923  apdifflemr  13926  iswomninnlem  13928  iswomninn  13929  ismkvnnlem  13931  ismkvnn  13932  redcwlpo  13934  dcapnconst  13939  nconstwlpolem0  13941  nconstwlpo  13944  neapmkv  13946  taupi  13949