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

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  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  640  notnoti  646  pm2.21i  647  pm2.24ii  648  notbii  670  nbn  701  ori  725  orci  733  olci  734  biorfi  748  imorri  751  dcbii  842  simp1i  1009  simp2i  1010  simp3i  1011  3mix1i  1172  3mix2i  1173  3mix3i  1174  3jaoi  1316  mptru  1382  dfnot  1391  mptnan  1443  mtpor  1445  mtpxor  1446  dcfromnotnotr  1468  dcfromcon  1469  dcfrompeirce  1470  mpg  1475  19.23h  1522  hbequid  1537  axi12  1538  nfri  1543  spi  1560  19.21  1607  eximii  1626  19.35i  1649  nfn  1682  19.37aiv  1699  19.23  1702  exan  1717  equid  1725  hbae  1742  equvini  1782  equveli  1783  sbid  1798  sbieh  1814  exdistrfor  1824  dveeq2or  1840  ax11v  1851  ax11ev  1852  equs5or  1854  sb4or  1857  sb4bor  1859  nfsb2or  1861  sbequilem  1862  sbequi  1863  speiv  1886  nfsbxy  1971  nfsbxyt  1972  sbco  1997  sbcocom  1999  sbcomxyyz  2001  sbal1yz  2030  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  eumoi  2088  moani  2126  elsb1  2185  elsb2  2186  eqeq1i  2215  eqeq2i  2218  eleq1i  2273  eleq2i  2274  nfcrii  2343  neeq1i  2393  neeq2i  2394  necon3i  2426  rspec  2560  rgen2a  2562  mprg  2565  r19.21  2584  r19.23  2616  raleqi  2709  rexeqi  2710  rabeqif  2767  elv  2780  elexi  2789  ceqsal  2806  vtocl3  2834  vtoclef  2853  vtocle  2854  spcv  2874  spcev  2875  clel3  2915  elabf  2923  elab2  2928  elab3  2932  euxfrdc  2966  reueq  2979  rmoimi2  2983  sbsbc  3009  sbc8g  3013  sbc6  3031  sbcie  3040  sbcrex  3085  csbvarg  3129  csbief  3146  csbie2  3151  sbnfc2  3162  sseli  3197  sselii  3198  sseq1i  3227  sseq2i  3228  difeq1i  3295  difeq2i  3296  uneq1i  3331  uneq2i  3332  ineq1i  3378  ineq2i  3379  ssinss1  3410  difdif2ss  3438  n0ii  3477  ne0ii  3478  vn0  3479  vn0m  3480  abf  3512  disj2  3524  difid  3537  0dif  3540  disjdif  3541  difin0  3542  undif1ss  3543  difdifdirss  3553  iftruei  3585  iffalsei  3588  ifbieq2i  3603  ifbieq12i  3605  pweqi  3630  pwid  3641  sneqi  3655  elsn  3659  elpr  3664  elsn2  3677  ralsn  3686  rexsn  3687  eltp  3691  rabrsndc  3711  preq1i  3723  preq2i  3724  prid1  3749  snnz  3762  snm  3763  prnz  3766  prm  3767  tpnz  3769  snss  3779  snsssn  3815  opeq1i  3836  opeq2i  3837  unieqi  3874  unissi  3887  inteqi  3903  intmin2  3925  intab  3928  intsn  3934  iinconstm  3950  iuniin  3951  iinss1  3953  iunxdif2  3990  ssiinf  3991  iinss  3993  iinss2  3994  iinab  4003  iundif2ss  4007  iindif2m  4009  iinin2m  4010  iunxsn  4018  iunxprg  4022  iinpw  4032  invdisjrab  4053  sndisj  4055  disjxsn  4057  breqi  4065  breq1i  4066  breq2i  4067  brab1  4107  opabbii  4127  truni  4172  bm1.3ii  4181  a9evsep  4182  ax9vsep  4183  zfnuleu  4184  axnul  4185  ssexi  4198  rabex  4204  rabex2  4206  elpw2  4217  pwnss  4219  iin0r  4229  intv  4230  pwex  4243  snex  4245  notnotsnex  4247  ord3ex  4250  dtruarb  4251  undifexmid  4253  intid  4286  opnzi  4297  copsexg  4306  opwo0id  4311  opelopabf  4339  epelc  4356  elon  4439  inton  4458  onn0  4465  onm  4466  elsuc  4471  elsuc2  4472  sucid  4482  iunsuc  4485  onordi  4491  ontrci  4492  onelssi  4494  eusvnf  4518  ssonunii  4555  sucex  4565  onssi  4581  onsuci  4582  ordtriexmidlem  4585  ordtriexmidlem2  4586  ordtriexmid  4587  ontriexmidim  4588  ordtri2orexmid  4589  2ordpr  4590  ontr2exmid  4591  onsucsssucexmid  4593  onsucelsucexmid  4596  regexmidlemm  4598  reg2exmid  4602  onirri  4609  ruALT  4617  onprc  4618  sucon  4619  dtru  4626  0elsucexmid  4631  ordpwsucexmid  4636  ordtri2or2exmid  4637  ontri2orexmidim  4638  dcextest  4647  omex  4659  find  4665  omelon  4675  nnoni  4677  limom  4680  nnregexmid  4687  omsinds  4688  xpeq1i  4713  xpeq2i  4714  0nelxp  4721  opthprc  4744  mosubop  4759  releqi  4776  relssi  4784  relin1  4811  relin2  4812  reldif  4813  inopab  4828  difopab  4829  xpiindim  4833  opabbi2dv  4845  ideq  4848  coeq1i  4855  coeq2i  4856  cnveqi  4871  eldm  4894  eldm2  4895  dmeqi  4898  dmv  4913  rneqi  4925  elrnmpti  4950  dmex  4964  rnex  4965  reseq1i  4974  reseq2i  4975  residm  5010  resex  5019  resmpt3  5027  imaeq1i  5038  imaeq2i  5039  elima  5046  imaex  5056  elimasn  5068  args  5070  epini  5072  dfse2  5074  eliniseg2  5081  relbrcnv  5082  cotr  5083  issref  5084  cnvsym  5085  asymref  5087  intirr  5088  codir  5090  qfto  5091  ssrnres  5144  cnveq0  5158  cnvsn0  5170  dmsnop  5175  rnsnop  5182  resdm2  5192  dfco2a  5202  cocnvcnv1  5212  coi2  5218  coires1  5219  cnvssrndm  5223  cossxp  5224  cocnvres  5226  relrelss  5228  relcoi2  5232  unidmrn  5234  dfdm2  5236  unixpm  5237  cnvexg  5239  cnvex  5240  cnviinm  5243  iotaval  5262  funeqi  5311  funi  5322  funres  5331  funcnvsn  5338  funcnvcnv  5352  funin  5364  funcnvres  5366  isarep2  5380  fneq1i  5387  fneq2i  5388  fndmi  5393  fnresdisj  5405  fnresi  5413  mpt0  5423  dmmpti  5425  feq1i  5438  feq2i  5439  fdmi  5453  fun2  5470  fssres  5473  resasplitss  5477  fintm  5483  fconst6  5497  f1ores  5559  foimacnv  5562  resdif  5566  funcocnv2  5569  f10d  5579  f1ovi  5584  fveq1i  5600  fveq2i  5602  0fv  5635  fvun1  5668  fvopab3ig  5676  fvmptss2  5677  mptrcl  5685  elfvmptrab1  5697  fndmdif  5708  fneqeql2  5712  f1oresrab  5768  fmptco  5769  funopsn  5785  fnressn  5793  fressnfv  5794  fmptap  5797  fvsnun1  5804  fvsnun2  5805  fsnunfv  5808  fconst2  5824  mptex  5833  riotabiia  5940  acexmidlema  5958  acexmidlemb  5959  acexmidlemcase  5962  acexmidlem2  5964  acexmidlemv  5965  oveq1i  5977  oveq2i  5978  oveqi  5980  oprabidlem  5998  0neqopab  6013  oprabbii  6023  oprabss  6054  mpompt  6060  funoprab  6068  fnoprab  6071  ovigg  6089  elmpocl  6164  resfunexgALT  6216  cofunexg  6217  mptexw  6221  opabex3d  6229  opabex3  6230  1st0  6253  2nd0  6254  op1st  6255  op2nd  6256  f1stres  6268  f2ndres  6269  fo1stresm  6270  fo2ndresm  6271  1stcof  6272  2ndcof  6273  1stexg  6276  2ndexg  6277  releldm2  6294  reldm  6295  dfoprab3  6300  mpomptsx  6306  mpompts  6307  fnmpoi  6312  dmmpo  6313  mpoexxg  6319  mpoexw  6322  1stconst  6330  2ndconst  6331  dfmpo  6332  algrflem  6338  algrflemg  6339  cnvoprab  6343  f1od2  6344  mpoxopn0yelv  6348  mpoxopoveq  6349  tposssxp  6358  brtpos2  6360  reldmtpos  6362  dftpos2  6370  dftpos4  6372  tpostpos  6373  tpostpos2  6374  tposfo  6380  tposf  6381  tposeqi  6386  tposex  6387  tposoprab  6389  issmo  6397  smores  6401  smores2  6403  iordsmo  6406  smo0  6407  tfrlem8  6427  tfrexlem  6443  tfr1onlem3  6447  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlemres  6458  tfri1dALT  6460  tfri2  6475  rdgisuc1  6493  rdg0  6496  frecfun  6504  frec0g  6506  freccllem  6511  frecfcllem  6513  frecsuclem  6515  frecrdg  6517  2on0  6535  xp01disj  6542  2oconcl  6548  fnoa  6556  oaexg  6557  fnom  6559  omexg  6560  fnoei  6561  oeiexg  6562  oei0  6568  oacl  6569  oasuc  6573  o1p1e2  6577  omsuc  6581  nna0r  6587  nnm0r  6588  1onn  6629  2onn  6630  3onn  6631  4onn  6632  2ssom  6633  eqerlem  6674  eceq2i  6681  elqs  6696  qsex  6702  ecqs  6707  iinerm  6717  th3qlem1  6747  th3q  6750  mapsn  6800  mapsnf1o3  6807  ixpiinm  6834  ixpssmap  6842  brdom  6862  f1dom  6874  enref  6879  dom2  6889  idssen  6891  ssdomg  6893  ensymi  6897  ensn1  6911  fiprc  6931  1domsn  6939  xpcomf1o  6945  xpcomco  6946  dom0  6960  0dom  6961  xpmapenlem  6971  phplem2  6975  php5  6980  snnen2og  6981  1nen2  6983  php5dom  6985  ssfilem  6998  ssfiexmid  6999  domfiexmid  7001  0fin  7007  diffitest  7010  findcard  7011  findcard2  7012  findcard2s  7013  isinfinf  7020  ac6sfi  7021  inffiexmid  7029  pw1fin  7033  unfiexmid  7041  xpfi  7055  fisseneq  7057  ssfirab  7059  residfi  7068  en1eqsn  7076  snexxph  7078  sbthlem2  7086  sbthlemi3  7087  sbthlemi6  7090  sbthlem7  7091  fi0  7103  supeq1i  7116  infeq1i  7141  djuexb  7172  djuf1olemr  7182  inresflem  7188  djuinr  7191  updjudhcoinlf  7208  updjudhcoinrg  7209  casefun  7213  caserel  7215  caseinj  7217  caseinl  7219  caseinr  7220  omp1eomlem  7222  endjusym  7224  difinfsn  7228  difinfinf  7229  djuinj  7234  0ct  7235  ctmlemr  7236  ctssdclemn0  7238  ctssdccl  7239  omct  7245  ctfoex  7246  finomni  7268  exmidomni  7270  fodjuomni  7277  ctssexmid  7278  fodjumkv  7288  nninfwlporlem  7301  nninfwlpoimlemg  7303  nninfwlpoim  7307  nninfinfwlpo  7308  card0  7321  ficardon  7322  exmidonfinlem  7332  dju1p1e2  7336  exmidfodomrlemim  7340  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  iftrueb01  7369  3nelsucpw1  7380  sucpw1nss3  7381  3nsssucpw1  7382  2onetap  7402  exmidmotap  7408  0npi  7461  dmaddpi  7473  dmmulpi  7474  1lt2pi  7488  0nnq  7512  1nq  7514  dmaddpq  7527  dmmulpq  7528  rec1nq  7543  1lt2nq  7554  halfnqq  7558  prarloclemarch2  7567  enq0enq  7579  nqnq0pi  7586  nnnq0lem1  7594  addnnnq0  7597  mulnnnq0  7598  nq0m0r  7604  addpinq1  7612  prarloclem5  7648  prarloclemcalc  7650  1pr  7702  1idprl  7738  1idpru  7739  ltexprlemm  7748  recexprlem1ssl  7781  recexprlem1ssu  7782  suplocexprlemell  7861  suplocexprlem2b  7862  suplocexprlemmu  7866  suplocexprlemdisj  7868  suplocexprlemloc  7869  suplocexprlemub  7871  suplocexprlemlub  7872  prsrlem1  7890  addsrpr  7893  mulsrpr  7894  gt0srpr  7896  0nsr  7897  0r  7898  1sr  7899  m1r  7900  m1m1sr  7909  caucvgsr  7950  suplocsrlempr  7955  addresr  7985  mulresr  7986  pitonnlem1  7993  peano1nnnn  8000  axi2m1  8023  axcnre  8029  peano5nnnn  8040  axcaucvg  8048  mpomulf  8097  mulridi  8109  mullidi  8110  pnfnre  8149  mnfnre  8150  pnfnemnf  8162  mnfxr  8164  rexri  8165  ltnri  8200  ltleii  8210  00id  8248  addridi  8249  addlidi  8250  0cnALT  8297  negeqi  8301  negicn  8308  neg0  8353  renegcli  8369  negcli  8375  negidi  8376  negnegi  8377  subidi  8378  subid1i  8379  negne0bi  8380  negrebi  8381  mul02i  8497  mul01i  8498  mulm1i  8510  leidi  8593  gt0ne0ii  8595  inelr  8692  msqge0i  8725  gt0ap0ii  8736  1div1e1  8812  div1i  8848  eqnegi  8849  recclapi  8850  recidapi  8851  divmulapi  8874  rerecclapi  8885  redivclapi  8887  rerecapb  8951  recgt0  8958  ltp1i  9013  divgt0ii  9027  ltmul1ii  9036  ltdiv1ii  9037  sup3exmid  9065  peano5nni  9074  nnrei  9080  1nn  9082  nngt0i  9101  neg1ap0  9180  2timesi  9201  times2i  9202  2nn  9233  3nn  9234  4nn  9235  5nn  9236  6nn  9237  7nn  9238  8nn  9239  9nn  9240  2muline0  9297  rehalfcli  9321  nn0ssre  9334  nnnn0i  9338  dfn2  9343  0nn0  9345  nn0ge0i  9357  zrei  9413  neg1z  9439  nn0negzi  9442  dfz2  9480  nneoi  9512  peano5uzi  9517  dfuzi  9518  nn0ind-raph  9525  deceq1i  9545  deceq2i  9546  10nn  9554  numltc  9564  eluzel2  9688  eluz1i  9690  nn0uz  9718  nnuz  9719  infrenegsupex  9750  lbzbi  9772  divfnzn  9777  qdivcl  9799  irrmul  9803  irrmulap  9804  cnref1o  9807  0ltpnf  9939  mnflt0  9941  0lepnf  9947  xrltnsym  9950  xrlttri3  9954  nltpnft  9971  ngtmnft  9974  xrrebnd  9976  xnegmnf  9986  xneg0  9988  xltnegi  9992  xaddmnf1  10005  xaddmnf2  10006  mnfaddpnf  10008  xaddid1  10019  xnn0lenn0nn0  10022  xnn0xadd0  10024  xposdif  10039  ixxex  10056  iooval2  10072  unirnioo  10130  ioorebasg  10132  elrege0  10133  fzval2  10168  fzen  10200  fzprval  10239  fztpval  10240  uzdisj  10250  ige2m1fz  10267  fz01or  10268  fz1ssfz0  10274  fz0sn  10278  fz0tp  10279  fz0to3un2pr  10280  fz0to4untppr  10281  nn0disj  10295  1fv  10296  4fvwrd4  10297  fzo0ss1  10333  fzo01  10382  fzo12sn  10383  fzo0to2pr  10384  fzo0to3tp  10385  fzo0to42pr  10386  zsupssdc  10418  qbtwnxr  10437  flval  10452  fldiv4lem1div2  10487  modqfrac  10519  modqmulnn  10524  q2txmodxeq0  10566  frecuzrdgdom  10600  frecuzrdgfun  10602  frecuzrdgsuct  10606  frechashgf1o  10610  nnct  10617  xnn0nnen  10619  fxnn0nninf  10621  0tonninf  10622  1tonninf  10623  iseqvalcbv  10641  ser0f  10716  0exp0e1  10726  qexpcl  10737  qexpclz  10742  m1expcl2  10743  1exp  10750  sqvali  10801  sqcli  10802  sqeq0i  10803  resqcli  10806  sq1  10815  neg1sqe1  10816  iexpcyc  10826  qsqeqor  10832  facnn  10909  fac0  10910  fac1  10911  fac2  10913  fac3  10914  fac4  10915  bcval  10931  bcm1k  10942  bcpasc  10948  bccl  10949  4bc3eq4  10955  4bc2eq6  10956  hashinfom  10960  hashennn  10962  hashfz1  10965  fihasheq0  10975  hash0  10978  hashsng  10980  fihashen1  10981  omgadd  10984  hashp1i  10992  hashxp  11008  fimaxq  11009  zfz1iso  11023  hash2en  11025  wrdexi  11044  wrdv  11047  wrdeqi  11054  wrd0  11056  lsw0  11078  ccatclab  11088  ccatidid  11104  s1prc  11115  ccat1st1st  11131  swrds1  11159  fnpfx  11168  swrdccatin2  11220  pfxccatin12lem2  11222  shftidt2  11258  cjexp  11319  re0  11321  im0  11322  re1  11323  im1  11324  cj0  11327  cji  11328  recli  11337  imcli  11338  cjcli  11339  replimi  11340  cjcji  11341  reim0bi  11342  rerebi  11343  cjrebi  11344  recji  11345  imcji  11346  cjmulrcli  11347  cjmulvali  11348  cjmulge0i  11349  renegi  11350  imnegi  11351  cjnegi  11352  addcji  11353  uzin2  11413  rexanuz  11414  rexfiuz  11415  sqrtrval  11426  sqrt0  11430  resqrexlemcalc3  11442  resqrexlemcvg  11445  resqrex  11452  abs0  11484  absi  11485  qabsor  11501  absimle  11510  recan  11535  caubnd2  11543  leabsi  11554  absrei  11555  sqrtpclii  11556  sqrtgt0ii  11557  absvalsqi  11566  absvalsq2i  11567  abscli  11568  absge0i  11569  absval2i  11570  abs00i  11571  absgt0api  11572  absnegi  11573  abscji  11574  releabsi  11575  infxrnegsupex  11689  xrbdtri  11702  cbvsum  11786  sumeq1i  11789  sum0  11814  isumz  11815  fisumss  11818  fsumsersdc  11821  fsumadd  11832  isumclim  11847  isumclim3  11849  fsumcnv  11863  modfsummodlem1  11882  fsumrelem  11897  binomlem  11909  binom  11910  arisum2  11925  expcnv  11930  0.999...  11947  prodf1f  11969  cbvprod  11984  prodeq1i  11987  zproddc  12005  zprodap0  12007  prod0  12011  fprodssdc  12016  prodsnf  12018  fprodcnv  12051  fprodge0  12063  fprodge1  12065  ef0lem  12086  esum  12088  ere  12096  ege2le3  12097  ef0  12098  eff2  12106  efsep  12117  reeff1  12126  sin0  12155  cos0  12156  ef01bndlem  12182  cos2bnd  12186  sincos1sgn  12191  sincos2sgn  12192  sin4lt0  12193  eirr  12205  0dvds  12237  dvds1  12279  z0even  12337  n2dvdsm1  12339  z2even  12340  n2dvds3  12341  ndvdssub  12356  ndvdsi  12359  flodddiv4  12362  bits0  12374  bitsfzo  12381  0bits  12385  m1bits  12386  bitsinv1lem  12387  bitsinv1  12388  gcddvds  12399  gcd1  12423  6gcd4e2  12431  bezoutlembi  12441  dfgcd3  12446  dfgcd2  12450  nninfctlemfo  12476  nninfct  12477  3lcm2e6woprm  12523  qredeu  12534  isprm2lem  12553  isprm3  12555  prm2orodd  12563  isprm5lem  12578  sqrt2irr0  12601  pw2dvds  12603  phicl2  12651  phi1  12656  dfphi2  12657  phiprmpw  12659  eulerthlemrprm  12666  eulerthlemh  12668  odzval  12679  oddprm  12697  pczpre  12735  pcdiv  12740  pc0  12742  pcqdiv  12745  pcrec  12746  pcexp  12747  pcxcl  12749  pcxqcl  12750  pcdvdstr  12765  pc2dvds  12768  dvdsprmpweqnn  12774  pcmpt  12781  qexpz  12790  pockthi  12796  1arith2  12806  4sqlemffi  12834  4sqlem11  12839  4sqlem13m  12841  4sqlem19  12847  dec2dvds  12849  dec5nprm  12852  modxai  12854  modxp1i  12856  numexp0  12860  numexp1  12861  ennnfonelemp1  12892  ennnfonelem1  12893  ennnfonelemkh  12898  ennnfonelemex  12900  ennnfonelemnn0  12908  ennnfonelemr  12909  exmidunben  12912  ctinfomlemom  12913  ctinfom  12914  ctinf  12916  qnnen  12917  omctfn  12929  omiunct  12930  ssnnctlemct  12932  nninfdc  12939  structcnvcnv  12963  structfun  12965  structfn  12966  ndxarg  12970  ndxid  12971  setsresg  12985  setsslnid  12999  basmex  13006  basmexd  13007  strleun  13051  strle1g  13053  prdsex  13216  prdsvallem  13219  prdsval  13220  prdsbaslemss  13221  imasaddfnlemg  13261  quslem  13271  xpsfrnel  13291  xpsff1o  13296  ismgmn0  13305  fn0g  13322  0g0  13323  fngsum  13335  idghm  13710  rhmfn  14049  rmodislmodlem  14227  rmodislmod  14228  lidlmex  14352  mopnset  14429  cntopex  14431  cnfldex  14436  cnfldbas  14437  mpocnfldadd  14438  mpocnfldmul  14440  cnfldcj  14442  cnfldtset  14443  cnfldle  14444  cnfldds  14445  cnring  14447  cnfld0  14448  cnfld1  14449  cnfldneg  14450  cnfldplusf  14451  cnfldsub  14452  cnfldmulg  14453  cnfldexp  14454  cnsubglem  14456  cnsubrglem  14457  gzsubrg  14459  gsumfzfsumlem0  14463  cnfldui  14466  zringring  14470  zringabl  14471  zringgrp  14472  zring1  14478  zringsubgval  14482  expghmap  14484  znval  14513  znle  14514  znbaslemnn  14516  znbas  14521  znzrh2  14523  znzrhval  14524  znzrhfo  14525  znleval  14530  znidom  14534  znidomb  14535  fnpsr  14544  psrelbas  14552  psradd  14556  psraddcl  14557  psr1clfi  14565  mplrcl  14571  mplbasss  14573  mpladd  14581  istopon  14600  topontopi  14603  toponunii  14604  toponrestid  14608  istps  14619  topontopn  14624  eltpsi  14628  eltg4i  14642  eltg3  14644  tg1  14646  tg2  14647  tgclb  14652  topnex  14673  sn0topon  14675  distps  14678  cldrcl  14689  sn0cld  14724  restco  14761  lmrcl  14778  ssidcn  14797  cnconst2  14820  cnptopresti  14825  cnptoprest  14826  txuni2  14843  txbas  14845  eltx  14846  txcnp  14858  upxp  14859  txcnmpt  14860  uptx  14861  txcn  14862  txrest  14863  txlm  14866  cnmptid  14868  cnmpt1st  14875  cnmpt2nd  14876  hmeofn  14889  psmetge0  14918  ismeti  14933  xmetunirn  14945  xmetge0  14952  unirnblps  15009  unirnbl  15010  mopnex  15092  qtopbasss  15108  retop  15111  uniretop  15112  iooretopg  15115  cnxmet  15118  cntoptopon  15119  cnbl0  15121  cnfldxms  15124  cnfldtps  15125  rexmet  15136  blssioo  15140  tgioo  15141  tgqioo  15142  cnopnap  15198  hovercncf  15233  limcresi  15253  dvfvalap  15268  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvcnp2cntop  15286  dvcoapbr  15294  dvexp2  15299  dvrecap  15300  dveflem  15313  dvef  15314  plyun0  15323  plyrecj  15350  dvply2  15354  reeff1o  15360  sin0pilem1  15368  sin0pilem2  15369  pilem3  15370  pigt2lt4  15371  pire  15373  sinhalfpilem  15378  pidiv2halves  15382  cosneghalfpi  15385  cospi  15387  efipi  15388  sin2pi  15390  cos2pi  15391  ef2pi  15392  cosq14gt0  15419  coseq00topi  15422  coseq0negpitopi  15423  sincos4thpi  15427  sincos6thpi  15429  sincos3rdpi  15430  pigt3  15431  cos02pilt1  15438  ioocosf1o  15441  dfrelog  15447  relogf1o  15448  relogcl  15449  relogiso  15460  rpcxpsqrt  15509  rpabscxpbnd  15527  2logb9irr  15558  2logb9irrALT  15561  sqrt2cxp2logb9e3  15562  2irrexpq  15563  2logb9irrap  15564  2irrexpqap  15565  mpodvdsmulf1o  15577  fsumdvdsmul  15578  perfectlem2  15587  lgsdir2lem1  15620  lgsdir2lem2  15621  lgsdir2lem4  15623  lgsdir2lem5  15624  lgsdi  15629  gausslemma2dlem0i  15649  gausslemma2dlem4  15656  lgseisenlem4  15665  lgsquadlem1  15669  lgsquad2lem2  15674  lgsquad2  15675  m1lgs  15677  2lgs2  15694  2lgslem4  15695  2lgsoddprmlem2  15698  2lgsoddprmlem3c  15701  2lgsoddprmlem3d  15702  2sqlem9  15716  2sqlem10  15717  1vgrex  15734  vtxval0  15765  iedgval0  15766  uhgr0  15796  upgrfi  15813  umgrislfupgrdom  15837  ex-fl  15861  ex-ceil  15862  ex-exp  15863  ex-fac  15864  ex-gcd  15867  bj-stfal  15878  bj-stst  15881  bj-dcfal  15891  bj-dcdc  15895  bj-stdc  15896  bj-dcst  15897  bj-el2oss1o  15910  elabf2  15918  bd0  15959  bdeli  15981  bdcriota  16018  bdbm1.3ii  16026  bdinex1  16034  bdssexi  16038  bj-inex  16042  bj-snex  16048  bj-sucex  16058  bj-d0clsepcl  16060  bj-omind  16069  bj-om  16072  bj-2inf  16073  bj-peano2  16074  bdpeano5  16078  bj-omssonALT  16098  bj-inf2vnlem1  16105  bj-omex2  16112  bj-nn0sucALT  16113  dom1o  16128  012of  16130  2o01f  16131  subctctexmid  16139  nninfall  16148  nninfsellemqall  16154  nninfsellemeqinf  16155  nninfomnilem  16157  nninfomni  16158  exmidsbthrlem  16163  sbthom  16167  isomninnlem  16171  isomninn  16172  cvgcmp2nlemabs  16173  iooreen  16176  trilpolemisumle  16179  trilpolemeq1  16181  trilpo  16184  trirec0  16185  apdifflemr  16188  iswomninnlem  16190  iswomninn  16191  ismkvnnlem  16193  ismkvnn  16194  redcwlpo  16196  dcapnconst  16202  nconstwlpolem0  16204  nconstwlpo  16207  neapmkv  16209  neap0mkv  16210  taupi  16214