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 𝜑 is true, and 𝜑 implies 𝜓, then 𝜓 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	⊢ 𝜑
maj	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ax-mp	⊢ 𝜓

Detailed syntax breakdown of Axiom ax-mp

Step	Hyp	Ref	Expression
1		wps	1 wff 𝜓

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  2231  eleq2i  2232  nfcrii  2300  neeq1i  2350  neeq2i  2351  necon3i  2383  rspec  2517  rgen2a  2519  mprg  2522  r19.21  2541  r19.23  2573  raleqi  2664  rexeqi  2665  rabeqif  2716  elv  2729  elexi  2737  ceqsal  2754  vtocl3  2781  vtoclef  2798  vtocle  2799  spcv  2819  spcev  2820  clel3  2860  elabf  2868  elab2  2873  elab3  2877  euxfrdc  2911  reueq  2924  rmoimi2  2928  sbsbc  2954  sbc8g  2957  sbc6  2975  sbcie  2984  sbcrex  3029  csbvarg  3072  csbief  3088  csbie2  3093  sbnfc2  3104  sseli  3137  sselii  3138  sseq1i  3167  sseq2i  3168  difeq1i  3235  difeq2i  3236  uneq1i  3271  uneq2i  3272  ineq1i  3318  ineq2i  3319  ssinss1  3350  difdif2ss  3378  n0ii  3416  ne0ii  3417  vn0  3418  vn0m  3419  abf  3451  disj2  3463  difid  3476  0dif  3479  disjdif  3480  difin0  3481  undif1ss  3482  difdifdirss  3492  rgenm  3510  iftruei  3525  iffalsei  3528  ifbieq2i  3542  ifbieq12i  3544  pweqi  3562  pwid  3573  sneqi  3587  elsn  3591  elpr  3596  elsn2  3609  ralsn  3618  rexsn  3619  eltp  3623  rabrsndc  3643  preq1i  3655  preq2i  3656  prid1  3681  snnz  3694  snm  3695  prnz  3697  prm  3698  tpnz  3700  snsssn  3740  opeq1i  3760  opeq2i  3761  unieqi  3798  unissi  3811  inteqi  3827  intmin2  3849  intab  3852  intsn  3858  iinconstm  3874  iuniin  3875  iinss1  3877  iunxdif2  3913  ssiinf  3914  iinss  3916  iinss2  3917  iinab  3926  iundif2ss  3930  iindif2m  3932  iinin2m  3933  iunxsn  3941  iunxprg  3945  iinpw  3955  sndisj  3977  disjxsn  3979  breqi  3987  breq1i  3988  breq2i  3989  brab1  4028  opabbii  4048  truni  4093  bm1.3ii  4102  a9evsep  4103  ax9vsep  4104  zfnuleu  4105  axnul  4106  ssexi  4119  rabex  4125  elpw2  4135  pwnss  4137  iin0r  4147  intv  4148  pwex  4161  snex  4163  notnotsnex  4165  ord3ex  4168  dtruarb  4169  undifexmid  4171  intid  4201  opnzi  4212  copsexg  4221  opelopabf  4251  epelc  4268  elon  4351  inton  4370  onn0  4377  onm  4378  elsuc  4383  elsuc2  4384  sucid  4394  iunsuc  4397  onordi  4403  ontrci  4404  onelssi  4406  eusvnf  4430  ssonunii  4465  sucex  4475  onssi  4491  onsuci  4492  ordtriexmidlem  4495  ordtriexmidlem2  4496  ordtriexmid  4497  ontriexmidim  4498  ordtri2orexmid  4499  2ordpr  4500  ontr2exmid  4501  onsucsssucexmid  4503  onsucelsucexmid  4506  regexmidlemm  4508  reg2exmid  4512  onirri  4519  ruALT  4527  onprc  4528  sucon  4529  dtru  4536  0elsucexmid  4541  ordpwsucexmid  4546  ordtri2or2exmid  4547  ontri2orexmidim  4548  dcextest  4557  omex  4569  find  4575  omelon  4585  nnoni  4587  limom  4590  nnregexmid  4597  omsinds  4598  xpeq1i  4623  xpeq2i  4624  0nelxp  4631  opthprc  4654  mosubop  4669  releqi  4686  relssi  4694  relin1  4721  relin2  4722  reldif  4723  inopab  4735  difopab  4736  xpiindim  4740  opabbi2dv  4752  ideq  4755  coeq1i  4762  coeq2i  4763  cnveqi  4778  eldm  4800  eldm2  4801  dmeqi  4804  dmv  4819  rneqi  4831  elrnmpti  4856  dmex  4869  rnex  4870  reseq1i  4879  reseq2i  4880  residm  4915  resex  4924  resmpt3  4932  imaeq1i  4942  imaeq2i  4943  elima  4950  imaex  4958  elimasn  4970  args  4972  epini  4974  dfse2  4976  relbrcnv  4983  cotr  4984  issref  4985  cnvsym  4986  asymref  4988  intirr  4989  codir  4991  qfto  4992  ssrnres  5045  cnveq0  5059  cnvsn0  5071  dmsnop  5076  rnsnop  5083  resdm2  5093  dfco2a  5103  cocnvcnv1  5113  coi2  5119  coires1  5120  cnvssrndm  5124  cossxp  5125  cocnvres  5127  relrelss  5129  relcoi2  5133  unidmrn  5135  dfdm2  5137  unixpm  5138  cnvexg  5140  cnvex  5141  cnviinm  5144  iotaval  5163  funeqi  5208  funi  5219  funres  5228  funcnvsn  5232  funcnvcnv  5246  funin  5258  funcnvres  5260  isarep2  5274  fneq1i  5281  fneq2i  5282  fnresdisj  5297  fnresi  5304  mpt0  5314  dmmpti  5316  feq1i  5329  feq2i  5330  fdmi  5344  fun2  5360  fssres  5362  resasplitss  5366  fintm  5372  fconst6  5386  f1ores  5446  foimacnv  5449  resdif  5453  funcocnv2  5456  f1ovi  5470  fveq1i  5486  fveq2i  5488  0fv  5520  fvun1  5551  fvopab3ig  5559  fvmptss2  5560  mptrcl  5567  elfvmptrab1  5579  fndmdif  5589  fneqeql2  5593  f1oresrab  5649  fmptco  5650  fnressn  5670  fressnfv  5671  fmptap  5674  fvsnun1  5681  fvsnun2  5682  fsnunfv  5685  fconst2  5701  mptex  5710  riotabiia  5814  acexmidlema  5832  acexmidlemb  5833  acexmidlemcase  5836  acexmidlem2  5838  acexmidlemv  5839  oveq1i  5851  oveq2i  5852  oveqi  5854  oprabidlem  5869  0neqopab  5883  oprabbii  5893  oprabss  5924  mpompt  5930  funoprab  5938  fnoprab  5941  fovcl  5943  ovigg  5958  elmpocl  6035  resfunexgALT  6075  cofunexg  6076  opabex3d  6086  opabex3  6087  1st0  6109  2nd0  6110  op1st  6111  op2nd  6112  f1stres  6124  f2ndres  6125  fo1stresm  6126  fo2ndresm  6127  1stcof  6128  2ndcof  6129  1stexg  6132  2ndexg  6133  releldm2  6150  reldm  6151  dfoprab3  6156  mpomptsx  6162  mpompts  6163  fnmpoi  6169  dmmpo  6170  mpoexxg  6175  1stconst  6185  2ndconst  6186  dfmpo  6187  algrflem  6193  algrflemg  6194  cnvoprab  6198  f1od2  6199  mpoxopn0yelv  6203  mpoxopoveq  6204  tposssxp  6213  brtpos2  6215  reldmtpos  6217  dftpos2  6225  dftpos4  6227  tpostpos  6228  tpostpos2  6229  tposfo  6235  tposf  6236  tposeqi  6241  tposex  6242  tposoprab  6244  issmo  6252  smores  6256  smores2  6258  iordsmo  6261  smo0  6262  tfrlem8  6282  tfrexlem  6298  tfr1onlem3  6302  tfr1onlemsucaccv  6305  tfr1onlembxssdm  6307  tfr1onlemres  6313  tfri1dALT  6315  tfri2  6330  rdgisuc1  6348  rdg0  6351  frecfun  6359  frec0g  6361  freccllem  6366  frecfcllem  6368  frecsuclem  6370  frecrdg  6372  2on0  6390  xp01disj  6397  2oconcl  6403  fnoa  6411  oaexg  6412  fnom  6414  omexg  6415  fnoei  6416  oeiexg  6417  oei0  6423  oacl  6424  oasuc  6428  o1p1e2  6432  omsuc  6436  nna0r  6442  nnm0r  6443  1onn  6484  2onn  6485  3onn  6486  4onn  6487  eqerlem  6528  elqs  6548  qsex  6554  ecqs  6559  iinerm  6569  th3qlem1  6599  th3q  6602  mapsn  6652  mapsnf1o3  6659  ixpiinm  6686  ixpssmap  6694  brdom  6712  f1dom  6722  enref  6727  dom2  6737  idssen  6739  ssdomg  6740  ensymi  6744  ensn1  6758  fiprc  6777  1domsn  6781  xpcomf1o  6787  xpcomco  6788  dom0  6800  0dom  6801  xpmapenlem  6811  phplem2  6815  php5  6820  snnen2og  6821  1nen2  6823  php5dom  6825  ssfilem  6837  ssfiexmid  6838  domfiexmid  6840  0fin  6846  diffitest  6849  findcard  6850  findcard2  6851  findcard2s  6852  isinfinf  6859  ac6sfi  6860  inffiexmid  6868  pw1fin  6872  unfiexmid  6879  xpfi  6891  fisseneq  6893  ssfirab  6895  en1eqsn  6909  snexxph  6911  sbthlem2  6919  sbthlemi3  6920  sbthlemi6  6923  sbthlem7  6924  fi0  6936  supeq1i  6949  infeq1i  6974  djuexb  7005  djuf1olemr  7015  inresflem  7021  djuinr  7024  updjudhcoinlf  7041  updjudhcoinrg  7042  casefun  7046  caserel  7048  caseinj  7050  caseinl  7052  caseinr  7053  omp1eomlem  7055  endjusym  7057  difinfsn  7061  difinfinf  7062  djuinj  7067  0ct  7068  ctmlemr  7069  ctssdclemn0  7071  ctssdccl  7072  omct  7078  ctfoex  7079  finomni  7100  exmidomni  7102  fodjuomni  7109  ctssexmid  7110  fodjumkv  7120  card0  7140  exmidonfinlem  7145  dju1p1e2  7149  exmidfodomrlemim  7153  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  3nelsucpw1  7186  sucpw1nss3  7187  3nsssucpw1  7188  0npi  7250  dmaddpi  7262  dmmulpi  7263  1lt2pi  7277  0nnq  7301  1nq  7303  dmaddpq  7316  dmmulpq  7317  rec1nq  7332  1lt2nq  7343  halfnqq  7347  prarloclemarch2  7356  enq0enq  7368  nqnq0pi  7375  nnnq0lem1  7383  addnnnq0  7386  mulnnnq0  7387  nq0m0r  7393  addpinq1  7401  prarloclem5  7437  prarloclemcalc  7439  1pr  7491  1idprl  7527  1idpru  7528  ltexprlemm  7537  recexprlem1ssl  7570  recexprlem1ssu  7571  suplocexprlemell  7650  suplocexprlem2b  7651  suplocexprlemmu  7655  suplocexprlemdisj  7657  suplocexprlemloc  7658  suplocexprlemub  7660  suplocexprlemlub  7661  prsrlem1  7679  addsrpr  7682  mulsrpr  7683  gt0srpr  7685  0nsr  7686  0r  7687  1sr  7688  m1r  7689  m1m1sr  7698  caucvgsr  7739  suplocsrlempr  7744  addresr  7774  mulresr  7775  pitonnlem1  7782  peano1nnnn  7789  axi2m1  7812  axcnre  7818  peano5nnnn  7829  axcaucvg  7837  mulid1i  7897  mulid2i  7898  pnfnre  7936  mnfnre  7937  pnfnemnf  7949  mnfxr  7951  rexri  7952  ltnri  7987  ltleii  7997  00id  8035  addid1i  8036  addid2i  8037  0cnALT  8084  negeqi  8088  negicn  8095  neg0  8140  renegcli  8156  negcli  8162  negidi  8163  negnegi  8164  subidi  8165  subid1i  8166  negne0bi  8167  negrebi  8168  mul02i  8284  mul01i  8285  mulm1i  8297  leidi  8379  gt0ne0ii  8381  inelr  8478  msqge0i  8511  gt0ap0ii  8522  1div1e1  8596  div1i  8632  eqnegi  8633  recclapi  8634  recidapi  8635  divmulapi  8658  rerecclapi  8669  redivclapi  8671  recgt0  8741  ltp1i  8796  divgt0ii  8810  ltmul1ii  8819  ltdiv1ii  8820  sup3exmid  8848  peano5nni  8856  nnrei  8862  1nn  8864  nngt0i  8883  neg1ap0  8962  2timesi  8983  times2i  8984  2nn  9014  3nn  9015  4nn  9016  5nn  9017  6nn  9018  7nn  9019  8nn  9020  9nn  9021  2muline0  9078  rehalfcli  9101  nn0ssre  9114  nnnn0i  9118  dfn2  9123  0nn0  9125  nn0ge0i  9137  zrei  9193  neg1z  9219  nn0negzi  9222  dfz2  9259  nneoi  9291  peano5uzi  9296  dfuzi  9297  nn0ind-raph  9304  deceq1i  9324  deceq2i  9325  10nn  9333  numltc  9343  eluzel2  9467  eluz1i  9469  nn0uz  9496  nnuz  9497  infrenegsupex  9528  lbzbi  9550  divfnzn  9555  qdivcl  9577  irrmul  9581  cnref1o  9584  0ltpnf  9714  mnflt0  9716  0lepnf  9722  xrltnsym  9725  xrlttri3  9729  nltpnft  9746  ngtmnft  9749  xrrebnd  9751  xnegmnf  9761  xneg0  9763  xltnegi  9767  xaddmnf1  9780  xaddmnf2  9781  mnfaddpnf  9783  xaddid1  9794  xnn0lenn0nn0  9797  xnn0xadd0  9799  xposdif  9814  ixxex  9831  iooval2  9847  unirnioo  9905  ioorebasg  9907  elrege0  9908  fzval2  9943  fzen  9974  fzprval  10013  fztpval  10014  uzdisj  10024  ige2m1fz  10041  fz01or  10042  fz1ssfz0  10048  fz0sn  10052  fz0tp  10053  fz0to3un2pr  10054  fz0to4untppr  10055  nn0disj  10069  1fv  10070  4fvwrd4  10071  fzo0ss1  10105  fzo01  10147  fzo12sn  10148  fzo0to2pr  10149  fzo0to3tp  10150  fzo0to42pr  10151  qbtwnxr  10189  flval  10203  modqfrac  10268  modqmulnn  10273  q2txmodxeq0  10315  frecuzrdgdom  10349  frecuzrdgfun  10351  frecuzrdgsuct  10355  frechashgf1o  10359  nnct  10366  fxnn0nninf  10369  0tonninf  10370  1tonninf  10371  iseqvalcbv  10388  ser0f  10446  0exp0e1  10456  qexpcl  10467  qexpclz  10472  m1expcl2  10473  1exp  10480  sqvali  10530  sqcli  10531  sqeq0i  10532  resqcli  10535  sq1  10544  neg1sqe1  10545  iexpcyc  10555  qsqeqor  10561  facnn  10636  fac0  10637  fac1  10638  fac2  10640  fac3  10641  fac4  10642  bcval  10658  bcm1k  10669  bcpasc  10675  bccl  10676  4bc3eq4  10682  4bc2eq6  10683  hashinfom  10687  hashennn  10689  hashfz1  10692  fihasheq0  10703  hash0  10706  hashsng  10707  fihashen1  10708  omgadd  10711  hashp1i  10719  hashxp  10735  fimaxq  10736  zfz1iso  10750  shftidt2  10770  cjexp  10831  re0  10833  im0  10834  re1  10835  im1  10836  cj0  10839  cji  10840  recli  10849  imcli  10850  cjcli  10851  replimi  10852  cjcji  10853  reim0bi  10854  rerebi  10855  cjrebi  10856  recji  10857  imcji  10858  cjmulrcli  10859  cjmulvali  10860  cjmulge0i  10861  renegi  10862  imnegi  10863  cjnegi  10864  addcji  10865  uzin2  10925  rexanuz  10926  rexfiuz  10927  sqrtrval  10938  sqrt0  10942  resqrexlemcalc3  10954  resqrexlemcvg  10957  resqrex  10964  abs0  10996  absi  10997  qabsor  11013  absimle  11022  recan  11047  caubnd2  11055  leabsi  11066  absrei  11067  sqrtpclii  11068  sqrtgt0ii  11069  absvalsqi  11078  absvalsq2i  11079  abscli  11080  absge0i  11081  absval2i  11082  abs00i  11083  absgt0api  11084  absnegi  11085  abscji  11086  releabsi  11087  infxrnegsupex  11200  xrbdtri  11213  cbvsum  11297  sumeq1i  11300  sum0  11325  isumz  11326  fisumss  11329  fsumsersdc  11332  fsumadd  11343  isumclim  11358  isumclim3  11360  fsumcnv  11374  modfsummodlem1  11393  fsumrelem  11408  binomlem  11420  binom  11421  arisum2  11436  expcnv  11441  0.999...  11458  prodf1f  11480  cbvprod  11495  prodeq1i  11498  zproddc  11516  zprodap0  11518  prod0  11522  fprodssdc  11527  prodsnf  11529  fprodcnv  11562  fprodge0  11574  fprodge1  11576  ef0lem  11597  esum  11599  ere  11607  ege2le3  11608  ef0  11609  eff2  11617  efsep  11628  reeff1  11637  sin0  11666  cos0  11667  ef01bndlem  11693  cos2bnd  11697  sincos1sgn  11701  sincos2sgn  11702  sin4lt0  11703  eirr  11715  0dvds  11747  dvds1  11787  z0even  11844  n2dvdsm1  11846  z2even  11847  n2dvds3  11848  ndvdssub  11863  ndvdsi  11866  flodddiv4  11867  zsupssdc  11883  gcddvds  11892  gcd1  11916  6gcd4e2  11924  bezoutlembi  11934  dfgcd3  11939  dfgcd2  11943  lcmval  11991  lcmcllem  11995  lcmledvds  11998  3lcm2e6woprm  12014  qredeu  12025  isprm2lem  12044  isprm3  12046  prm2orodd  12054  isprm5lem  12069  sqrt2irr0  12092  pw2dvds  12094  phicl2  12142  phi1  12147  dfphi2  12148  phiprmpw  12150  eulerthlemrprm  12157  eulerthlemh  12159  odzval  12169  oddprm  12187  pczpre  12225  pcdiv  12230  pc0  12232  pcqdiv  12235  pcrec  12236  pcexp  12237  pcxcl  12239  pcdvdstr  12254  pc2dvds  12257  dvdsprmpweqnn  12263  pcmpt  12269  qexpz  12278  pockthi  12284  1arith2  12294  ennnfonelemp1  12335  ennnfonelem1  12336  ennnfonelemkh  12341  ennnfonelemex  12343  ennnfonelemnn0  12351  ennnfonelemr  12352  exmidunben  12355  ctinfomlemom  12356  ctinfom  12357  ctinf  12359  qnnen  12360  omctfn  12372  omiunct  12373  ssnnctlemct  12375  nninfdc  12382  structcnvcnv  12406  structfun  12408  structfn  12409  ndxarg  12413  ndxid  12414  setsresg  12428  setsslnid  12441  strleun  12479  strle1g  12480  istopon  12611  topontopi  12614  toponunii  12615  toponrestid  12619  istps  12630  topontopn  12635  eltpsi  12639  eltg4i  12655  eltg3  12657  tg1  12659  tg2  12660  tgclb  12665  topnex  12686  sn0topon  12688  distps  12691  cldrcl  12702  sn0cld  12737  restco  12774  lmrcl  12791  ssidcn  12810  cnconst2  12833  cnptopresti  12838  cnptoprest  12839  txuni2  12856  txbas  12858  eltx  12859  txcnp  12871  upxp  12872  txcnmpt  12873  uptx  12874  txcn  12875  txrest  12876  txlm  12879  cnmptid  12881  cnmpt1st  12888  cnmpt2nd  12889  hmeofn  12902  psmetge0  12931  ismeti  12946  xmetunirn  12958  xmetge0  12965  unirnblps  13022  unirnbl  13023  mopnex  13105  qtopbasss  13121  retop  13124  uniretop  13125  iooretopg  13128  cnxmet  13131  cntoptopon  13132  cnbl0  13134  rexmet  13141  blssioo  13145  tgioo  13146  tgqioo  13147  cnopnap  13194  limcresi  13235  dvfvalap  13250  dvidlemap  13260  dvcnp2cntop  13263  dvcoapbr  13271  dvexp2  13276  dvrecap  13277  dveflem  13287  dvef  13288  reeff1o  13294  sin0pilem1  13302  sin0pilem2  13303  pilem3  13304  pigt2lt4  13305  pire  13307  sinhalfpilem  13312  pidiv2halves  13316  cosneghalfpi  13319  cospi  13321  efipi  13322  sin2pi  13324  cos2pi  13325  ef2pi  13326  cosq14gt0  13353  coseq00topi  13356  coseq0negpitopi  13357  sincos4thpi  13361  sincos6thpi  13363  sincos3rdpi  13364  pigt3  13365  cos02pilt1  13372  ioocosf1o  13375  dfrelog  13381  relogf1o  13382  relogcl  13383  relogiso  13394  rpcxpsqrt  13442  rpabscxpbnd  13459  2logb9irr  13489  2logb9irrALT  13492  sqrt2cxp2logb9e3  13493  2irrexpq  13494  2logb9irrap  13495  2irrexpqap  13496  lgsdir2lem1  13529  lgsdir2lem2  13530  lgsdir2lem4  13532  lgsdir2lem5  13533  lgsdi  13538  2sqlem9  13560  2sqlem10  13561  ex-fl  13566  ex-ceil  13567  ex-exp  13568  ex-fac  13569  ex-gcd  13572  bj-stfal  13583  bj-stst  13586  bj-dcfal  13596  bj-dcdc  13600  bj-stdc  13601  bj-dcst  13602  bj-el2oss1o  13615  elabf2  13623  2ssom  13644  bd0  13666  bdeli  13688  bdcriota  13725  bdbm1.3ii  13733  bdinex1  13741  bdssexi  13745  bj-inex  13749  bj-snex  13755  bj-sucex  13765  bj-d0clsepcl  13767  bj-omind  13776  bj-om  13779  bj-2inf  13780  bj-peano2  13781  bdpeano5  13785  bj-omssonALT  13805  bj-inf2vnlem1  13812  bj-omex2  13819  bj-nn0sucALT  13820  012of  13835  2o01f  13836  subctctexmid  13841  nninfall  13849  nninfsellemqall  13855  nninfsellemeqinf  13856  nninfomnilem  13858  nninfomni  13859  exmidsbthrlem  13861  sbthom  13865  isomninnlem  13869  isomninn  13870  cvgcmp2nlemabs  13871  iooreen  13874  trilpolemisumle  13877  trilpolemeq1  13879  trilpo  13882  trirec0  13883  apdifflemr  13886  iswomninnlem  13888  iswomninn  13889  ismkvnnlem  13891  ismkvnn  13892  redcwlpo  13894  dcapnconst  13899  nconstwlpolem0  13901  nconstwlpo  13904  neapmkv  13906  taupi  13909