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  3423  ne0ii  3424  vn0  3425  vn0m  3426  abf  3458  disj2  3470  difid  3483  0dif  3486  disjdif  3487  difin0  3488  undif1ss  3489  difdifdirss  3499  rgenm  3517  iftruei  3532  iffalsei  3535  ifbieq2i  3549  ifbieq12i  3551  pweqi  3570  pwid  3581  sneqi  3595  elsn  3599  elpr  3604  elsn2  3617  ralsn  3626  rexsn  3627  eltp  3631  rabrsndc  3651  preq1i  3663  preq2i  3664  prid1  3689  snnz  3702  snm  3703  prnz  3705  prm  3706  tpnz  3708  snsssn  3748  opeq1i  3768  opeq2i  3769  unieqi  3806  unissi  3819  inteqi  3835  intmin2  3857  intab  3860  intsn  3866  iinconstm  3882  iuniin  3883  iinss1  3885  iunxdif2  3921  ssiinf  3922  iinss  3924  iinss2  3925  iinab  3934  iundif2ss  3938  iindif2m  3940  iinin2m  3941  iunxsn  3949  iunxprg  3953  iinpw  3963  sndisj  3985  disjxsn  3987  breqi  3995  breq1i  3996  breq2i  3997  brab1  4036  opabbii  4056  truni  4101  bm1.3ii  4110  a9evsep  4111  ax9vsep  4112  zfnuleu  4113  axnul  4114  ssexi  4127  rabex  4133  elpw2  4143  pwnss  4145  iin0r  4155  intv  4156  pwex  4169  snex  4171  notnotsnex  4173  ord3ex  4176  dtruarb  4177  undifexmid  4179  intid  4209  opnzi  4220  copsexg  4229  opelopabf  4259  epelc  4276  elon  4359  inton  4378  onn0  4385  onm  4386  elsuc  4391  elsuc2  4392  sucid  4402  iunsuc  4405  onordi  4411  ontrci  4412  onelssi  4414  eusvnf  4438  ssonunii  4473  sucex  4483  onssi  4499  onsuci  4500  ordtriexmidlem  4503  ordtriexmidlem2  4504  ordtriexmid  4505  ontriexmidim  4506  ordtri2orexmid  4507  2ordpr  4508  ontr2exmid  4509  onsucsssucexmid  4511  onsucelsucexmid  4514  regexmidlemm  4516  reg2exmid  4520  onirri  4527  ruALT  4535  onprc  4536  sucon  4537  dtru  4544  0elsucexmid  4549  ordpwsucexmid  4554  ordtri2or2exmid  4555  ontri2orexmidim  4556  dcextest  4565  omex  4577  find  4583  omelon  4593  nnoni  4595  limom  4598  nnregexmid  4605  omsinds  4606  xpeq1i  4631  xpeq2i  4632  0nelxp  4639  opthprc  4662  mosubop  4677  releqi  4694  relssi  4702  relin1  4729  relin2  4730  reldif  4731  inopab  4743  difopab  4744  xpiindim  4748  opabbi2dv  4760  ideq  4763  coeq1i  4770  coeq2i  4771  cnveqi  4786  eldm  4808  eldm2  4809  dmeqi  4812  dmv  4827  rneqi  4839  elrnmpti  4864  dmex  4877  rnex  4878  reseq1i  4887  reseq2i  4888  residm  4923  resex  4932  resmpt3  4940  imaeq1i  4950  imaeq2i  4951  elima  4958  imaex  4966  elimasn  4978  args  4980  epini  4982  dfse2  4984  relbrcnv  4991  cotr  4992  issref  4993  cnvsym  4994  asymref  4996  intirr  4997  codir  4999  qfto  5000  ssrnres  5053  cnveq0  5067  cnvsn0  5079  dmsnop  5084  rnsnop  5091  resdm2  5101  dfco2a  5111  cocnvcnv1  5121  coi2  5127  coires1  5128  cnvssrndm  5132  cossxp  5133  cocnvres  5135  relrelss  5137  relcoi2  5141  unidmrn  5143  dfdm2  5145  unixpm  5146  cnvexg  5148  cnvex  5149  cnviinm  5152  iotaval  5171  funeqi  5219  funi  5230  funres  5239  funcnvsn  5243  funcnvcnv  5257  funin  5269  funcnvres  5271  isarep2  5285  fneq1i  5292  fneq2i  5293  fnresdisj  5308  fnresi  5315  mpt0  5325  dmmpti  5327  feq1i  5340  feq2i  5341  fdmi  5355  fun2  5371  fssres  5373  resasplitss  5377  fintm  5383  fconst6  5397  f1ores  5457  foimacnv  5460  resdif  5464  funcocnv2  5467  f1ovi  5481  fveq1i  5497  fveq2i  5499  0fv  5531  fvun1  5562  fvopab3ig  5570  fvmptss2  5571  mptrcl  5578  elfvmptrab1  5590  fndmdif  5601  fneqeql2  5605  f1oresrab  5661  fmptco  5662  fnressn  5682  fressnfv  5683  fmptap  5686  fvsnun1  5693  fvsnun2  5694  fsnunfv  5697  fconst2  5713  mptex  5722  riotabiia  5826  acexmidlema  5844  acexmidlemb  5845  acexmidlemcase  5848  acexmidlem2  5850  acexmidlemv  5851  oveq1i  5863  oveq2i  5864  oveqi  5866  oprabidlem  5884  0neqopab  5898  oprabbii  5908  oprabss  5939  mpompt  5945  funoprab  5953  fnoprab  5956  fovcl  5958  ovigg  5973  elmpocl  6047  resfunexgALT  6087  cofunexg  6088  mptexw  6092  opabex3d  6100  opabex3  6101  1st0  6123  2nd0  6124  op1st  6125  op2nd  6126  f1stres  6138  f2ndres  6139  fo1stresm  6140  fo2ndresm  6141  1stcof  6142  2ndcof  6143  1stexg  6146  2ndexg  6147  releldm2  6164  reldm  6165  dfoprab3  6170  mpomptsx  6176  mpompts  6177  fnmpoi  6183  dmmpo  6184  mpoexxg  6189  mpoexw  6192  1stconst  6200  2ndconst  6201  dfmpo  6202  algrflem  6208  algrflemg  6209  cnvoprab  6213  f1od2  6214  mpoxopn0yelv  6218  mpoxopoveq  6219  tposssxp  6228  brtpos2  6230  reldmtpos  6232  dftpos2  6240  dftpos4  6242  tpostpos  6243  tpostpos2  6244  tposfo  6250  tposf  6251  tposeqi  6256  tposex  6257  tposoprab  6259  issmo  6267  smores  6271  smores2  6273  iordsmo  6276  smo0  6277  tfrlem8  6297  tfrexlem  6313  tfr1onlem3  6317  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlemres  6328  tfri1dALT  6330  tfri2  6345  rdgisuc1  6363  rdg0  6366  frecfun  6374  frec0g  6376  freccllem  6381  frecfcllem  6383  frecsuclem  6385  frecrdg  6387  2on0  6405  xp01disj  6412  2oconcl  6418  fnoa  6426  oaexg  6427  fnom  6429  omexg  6430  fnoei  6431  oeiexg  6432  oei0  6438  oacl  6439  oasuc  6443  o1p1e2  6447  omsuc  6451  nna0r  6457  nnm0r  6458  1onn  6499  2onn  6500  3onn  6501  4onn  6502  2ssom  6503  eqerlem  6544  elqs  6564  qsex  6570  ecqs  6575  iinerm  6585  th3qlem1  6615  th3q  6618  mapsn  6668  mapsnf1o3  6675  ixpiinm  6702  ixpssmap  6710  brdom  6728  f1dom  6738  enref  6743  dom2  6753  idssen  6755  ssdomg  6756  ensymi  6760  ensn1  6774  fiprc  6793  1domsn  6797  xpcomf1o  6803  xpcomco  6804  dom0  6816  0dom  6817  xpmapenlem  6827  phplem2  6831  php5  6836  snnen2og  6837  1nen2  6839  php5dom  6841  ssfilem  6853  ssfiexmid  6854  domfiexmid  6856  0fin  6862  diffitest  6865  findcard  6866  findcard2  6867  findcard2s  6868  isinfinf  6875  ac6sfi  6876  inffiexmid  6884  pw1fin  6888  unfiexmid  6895  xpfi  6907  fisseneq  6909  ssfirab  6911  en1eqsn  6925  snexxph  6927  sbthlem2  6935  sbthlemi3  6936  sbthlemi6  6939  sbthlem7  6940  fi0  6952  supeq1i  6965  infeq1i  6990  djuexb  7021  djuf1olemr  7031  inresflem  7037  djuinr  7040  updjudhcoinlf  7057  updjudhcoinrg  7058  casefun  7062  caserel  7064  caseinj  7066  caseinl  7068  caseinr  7069  omp1eomlem  7071  endjusym  7073  difinfsn  7077  difinfinf  7078  djuinj  7083  0ct  7084  ctmlemr  7085  ctssdclemn0  7087  ctssdccl  7088  omct  7094  ctfoex  7095  finomni  7116  exmidomni  7118  fodjuomni  7125  ctssexmid  7126  fodjumkv  7136  nninfwlporlem  7149  nninfwlpoimlemg  7151  nninfwlpoim  7154  card0  7165  exmidonfinlem  7170  dju1p1e2  7174  exmidfodomrlemim  7178  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  3nelsucpw1  7211  sucpw1nss3  7212  3nsssucpw1  7213  0npi  7275  dmaddpi  7287  dmmulpi  7288  1lt2pi  7302  0nnq  7326  1nq  7328  dmaddpq  7341  dmmulpq  7342  rec1nq  7357  1lt2nq  7368  halfnqq  7372  prarloclemarch2  7381  enq0enq  7393  nqnq0pi  7400  nnnq0lem1  7408  addnnnq0  7411  mulnnnq0  7412  nq0m0r  7418  addpinq1  7426  prarloclem5  7462  prarloclemcalc  7464  1pr  7516  1idprl  7552  1idpru  7553  ltexprlemm  7562  recexprlem1ssl  7595  recexprlem1ssu  7596  suplocexprlemell  7675  suplocexprlem2b  7676  suplocexprlemmu  7680  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemub  7685  suplocexprlemlub  7686  prsrlem1  7704  addsrpr  7707  mulsrpr  7708  gt0srpr  7710  0nsr  7711  0r  7712  1sr  7713  m1r  7714  m1m1sr  7723  caucvgsr  7764  suplocsrlempr  7769  addresr  7799  mulresr  7800  pitonnlem1  7807  peano1nnnn  7814  axi2m1  7837  axcnre  7843  peano5nnnn  7854  axcaucvg  7862  mulid1i  7922  mulid2i  7923  pnfnre  7961  mnfnre  7962  pnfnemnf  7974  mnfxr  7976  rexri  7977  ltnri  8012  ltleii  8022  00id  8060  addid1i  8061  addid2i  8062  0cnALT  8109  negeqi  8113  negicn  8120  neg0  8165  renegcli  8181  negcli  8187  negidi  8188  negnegi  8189  subidi  8190  subid1i  8191  negne0bi  8192  negrebi  8193  mul02i  8309  mul01i  8310  mulm1i  8322  leidi  8404  gt0ne0ii  8406  inelr  8503  msqge0i  8536  gt0ap0ii  8547  1div1e1  8621  div1i  8657  eqnegi  8658  recclapi  8659  recidapi  8660  divmulapi  8683  rerecclapi  8694  redivclapi  8696  recgt0  8766  ltp1i  8821  divgt0ii  8835  ltmul1ii  8844  ltdiv1ii  8845  sup3exmid  8873  peano5nni  8881  nnrei  8887  1nn  8889  nngt0i  8908  neg1ap0  8987  2timesi  9008  times2i  9009  2nn  9039  3nn  9040  4nn  9041  5nn  9042  6nn  9043  7nn  9044  8nn  9045  9nn  9046  2muline0  9103  rehalfcli  9126  nn0ssre  9139  nnnn0i  9143  dfn2  9148  0nn0  9150  nn0ge0i  9162  zrei  9218  neg1z  9244  nn0negzi  9247  dfz2  9284  nneoi  9316  peano5uzi  9321  dfuzi  9322  nn0ind-raph  9329  deceq1i  9349  deceq2i  9350  10nn  9358  numltc  9368  eluzel2  9492  eluz1i  9494  nn0uz  9521  nnuz  9522  infrenegsupex  9553  lbzbi  9575  divfnzn  9580  qdivcl  9602  irrmul  9606  cnref1o  9609  0ltpnf  9739  mnflt0  9741  0lepnf  9747  xrltnsym  9750  xrlttri3  9754  nltpnft  9771  ngtmnft  9774  xrrebnd  9776  xnegmnf  9786  xneg0  9788  xltnegi  9792  xaddmnf1  9805  xaddmnf2  9806  mnfaddpnf  9808  xaddid1  9819  xnn0lenn0nn0  9822  xnn0xadd0  9824  xposdif  9839  ixxex  9856  iooval2  9872  unirnioo  9930  ioorebasg  9932  elrege0  9933  fzval2  9968  fzen  9999  fzprval  10038  fztpval  10039  uzdisj  10049  ige2m1fz  10066  fz01or  10067  fz1ssfz0  10073  fz0sn  10077  fz0tp  10078  fz0to3un2pr  10079  fz0to4untppr  10080  nn0disj  10094  1fv  10095  4fvwrd4  10096  fzo0ss1  10130  fzo01  10172  fzo12sn  10173  fzo0to2pr  10174  fzo0to3tp  10175  fzo0to42pr  10176  qbtwnxr  10214  flval  10228  modqfrac  10293  modqmulnn  10298  q2txmodxeq0  10340  frecuzrdgdom  10374  frecuzrdgfun  10376  frecuzrdgsuct  10380  frechashgf1o  10384  nnct  10391  fxnn0nninf  10394  0tonninf  10395  1tonninf  10396  iseqvalcbv  10413  ser0f  10471  0exp0e1  10481  qexpcl  10492  qexpclz  10497  m1expcl2  10498  1exp  10505  sqvali  10555  sqcli  10556  sqeq0i  10557  resqcli  10560  sq1  10569  neg1sqe1  10570  iexpcyc  10580  qsqeqor  10586  facnn  10661  fac0  10662  fac1  10663  fac2  10665  fac3  10666  fac4  10667  bcval  10683  bcm1k  10694  bcpasc  10700  bccl  10701  4bc3eq4  10707  4bc2eq6  10708  hashinfom  10712  hashennn  10714  hashfz1  10717  fihasheq0  10728  hash0  10731  hashsng  10733  fihashen1  10734  omgadd  10737  hashp1i  10745  hashxp  10761  fimaxq  10762  zfz1iso  10776  shftidt2  10796  cjexp  10857  re0  10859  im0  10860  re1  10861  im1  10862  cj0  10865  cji  10866  recli  10875  imcli  10876  cjcli  10877  replimi  10878  cjcji  10879  reim0bi  10880  rerebi  10881  cjrebi  10882  recji  10883  imcji  10884  cjmulrcli  10885  cjmulvali  10886  cjmulge0i  10887  renegi  10888  imnegi  10889  cjnegi  10890  addcji  10891  uzin2  10951  rexanuz  10952  rexfiuz  10953  sqrtrval  10964  sqrt0  10968  resqrexlemcalc3  10980  resqrexlemcvg  10983  resqrex  10990  abs0  11022  absi  11023  qabsor  11039  absimle  11048  recan  11073  caubnd2  11081  leabsi  11092  absrei  11093  sqrtpclii  11094  sqrtgt0ii  11095  absvalsqi  11104  absvalsq2i  11105  abscli  11106  absge0i  11107  absval2i  11108  abs00i  11109  absgt0api  11110  absnegi  11111  abscji  11112  releabsi  11113  infxrnegsupex  11226  xrbdtri  11239  cbvsum  11323  sumeq1i  11326  sum0  11351  isumz  11352  fisumss  11355  fsumsersdc  11358  fsumadd  11369  isumclim  11384  isumclim3  11386  fsumcnv  11400  modfsummodlem1  11419  fsumrelem  11434  binomlem  11446  binom  11447  arisum2  11462  expcnv  11467  0.999...  11484  prodf1f  11506  cbvprod  11521  prodeq1i  11524  zproddc  11542  zprodap0  11544  prod0  11548  fprodssdc  11553  prodsnf  11555  fprodcnv  11588  fprodge0  11600  fprodge1  11602  ef0lem  11623  esum  11625  ere  11633  ege2le3  11634  ef0  11635  eff2  11643  efsep  11654  reeff1  11663  sin0  11692  cos0  11693  ef01bndlem  11719  cos2bnd  11723  sincos1sgn  11727  sincos2sgn  11728  sin4lt0  11729  eirr  11741  0dvds  11773  dvds1  11813  z0even  11870  n2dvdsm1  11872  z2even  11873  n2dvds3  11874  ndvdssub  11889  ndvdsi  11892  flodddiv4  11893  zsupssdc  11909  gcddvds  11918  gcd1  11942  6gcd4e2  11950  bezoutlembi  11960  dfgcd3  11965  dfgcd2  11969  lcmval  12017  lcmcllem  12021  lcmledvds  12024  3lcm2e6woprm  12040  qredeu  12051  isprm2lem  12070  isprm3  12072  prm2orodd  12080  isprm5lem  12095  sqrt2irr0  12118  pw2dvds  12120  phicl2  12168  phi1  12173  dfphi2  12174  phiprmpw  12176  eulerthlemrprm  12183  eulerthlemh  12185  odzval  12195  oddprm  12213  pczpre  12251  pcdiv  12256  pc0  12258  pcqdiv  12261  pcrec  12262  pcexp  12263  pcxcl  12265  pcdvdstr  12280  pc2dvds  12283  dvdsprmpweqnn  12289  pcmpt  12295  qexpz  12304  pockthi  12310  1arith2  12320  ennnfonelemp1  12361  ennnfonelem1  12362  ennnfonelemkh  12367  ennnfonelemex  12369  ennnfonelemnn0  12377  ennnfonelemr  12378  exmidunben  12381  ctinfomlemom  12382  ctinfom  12383  ctinf  12385  qnnen  12386  omctfn  12398  omiunct  12399  ssnnctlemct  12401  nninfdc  12408  structcnvcnv  12432  structfun  12434  structfn  12435  ndxarg  12439  ndxid  12440  setsresg  12454  setsslnid  12467  basmex  12474  basmexd  12475  strleun  12507  strle1g  12508  ismgmn0  12612  fn0g  12629  0g0  12630  istopon  12805  topontopi  12808  toponunii  12809  toponrestid  12813  istps  12824  topontopn  12829  eltpsi  12833  eltg4i  12849  eltg3  12851  tg1  12853  tg2  12854  tgclb  12859  topnex  12880  sn0topon  12882  distps  12885  cldrcl  12896  sn0cld  12931  restco  12968  lmrcl  12985  ssidcn  13004  cnconst2  13027  cnptopresti  13032  cnptoprest  13033  txuni2  13050  txbas  13052  eltx  13053  txcnp  13065  upxp  13066  txcnmpt  13067  uptx  13068  txcn  13069  txrest  13070  txlm  13073  cnmptid  13075  cnmpt1st  13082  cnmpt2nd  13083  hmeofn  13096  psmetge0  13125  ismeti  13140  xmetunirn  13152  xmetge0  13159  unirnblps  13216  unirnbl  13217  mopnex  13299  qtopbasss  13315  retop  13318  uniretop  13319  iooretopg  13322  cnxmet  13325  cntoptopon  13326  cnbl0  13328  rexmet  13335  blssioo  13339  tgioo  13340  tgqioo  13341  cnopnap  13388  limcresi  13429  dvfvalap  13444  dvidlemap  13454  dvcnp2cntop  13457  dvcoapbr  13465  dvexp2  13470  dvrecap  13471  dveflem  13481  dvef  13482  reeff1o  13488  sin0pilem1  13496  sin0pilem2  13497  pilem3  13498  pigt2lt4  13499  pire  13501  sinhalfpilem  13506  pidiv2halves  13510  cosneghalfpi  13513  cospi  13515  efipi  13516  sin2pi  13518  cos2pi  13519  ef2pi  13520  cosq14gt0  13547  coseq00topi  13550  coseq0negpitopi  13551  sincos4thpi  13555  sincos6thpi  13557  sincos3rdpi  13558  pigt3  13559  cos02pilt1  13566  ioocosf1o  13569  dfrelog  13575  relogf1o  13576  relogcl  13577  relogiso  13588  rpcxpsqrt  13636  rpabscxpbnd  13653  2logb9irr  13683  2logb9irrALT  13686  sqrt2cxp2logb9e3  13687  2irrexpq  13688  2logb9irrap  13689  2irrexpqap  13690  lgsdir2lem1  13723  lgsdir2lem2  13724  lgsdir2lem4  13726  lgsdir2lem5  13727  lgsdi  13732  2sqlem9  13754  2sqlem10  13755  ex-fl  13760  ex-ceil  13761  ex-exp  13762  ex-fac  13763  ex-gcd  13766  bj-stfal  13777  bj-stst  13780  bj-dcfal  13790  bj-dcdc  13794  bj-stdc  13795  bj-dcst  13796  bj-el2oss1o  13809  elabf2  13817  bd0  13859  bdeli  13881  bdcriota  13918  bdbm1.3ii  13926  bdinex1  13934  bdssexi  13938  bj-inex  13942  bj-snex  13948  bj-sucex  13958  bj-d0clsepcl  13960  bj-omind  13969  bj-om  13972  bj-2inf  13973  bj-peano2  13974  bdpeano5  13978  bj-omssonALT  13998  bj-inf2vnlem1  14005  bj-omex2  14012  bj-nn0sucALT  14013  012of  14028  2o01f  14029  subctctexmid  14034  nninfall  14042  nninfsellemqall  14048  nninfsellemeqinf  14049  nninfomnilem  14051  nninfomni  14052  exmidsbthrlem  14054  sbthom  14058  isomninnlem  14062  isomninn  14063  cvgcmp2nlemabs  14064  iooreen  14067  trilpolemisumle  14070  trilpolemeq1  14072  trilpo  14075  trirec0  14076  apdifflemr  14079  iswomninnlem  14081  iswomninn  14082  ismkvnnlem  14084  ismkvnn  14085  redcwlpo  14087  dcapnconst  14092  nconstwlpolem0  14094  nconstwlpo  14097  neapmkv  14099  taupi  14102