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

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  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  642  notnoti  648  pm2.21i  649  pm2.24ii  650  notbii  672  nbn  704  ori  728  orci  736  olci  737  biorfi  751  imorri  754  dcbii  845  simp1i  1030  simp2i  1031  simp3i  1032  3mix1i  1193  3mix2i  1194  3mix3i  1195  3jaoi  1337  mptru  1404  dfnot  1413  mptnan  1465  mtpor  1467  mtpxor  1468  dcfromnotnotr  1490  dcfromcon  1491  dcfrompeirce  1492  mpg  1497  19.23h  1544  hbequid  1559  axi12  1560  nfri  1565  spi  1582  19.21  1629  eximii  1648  19.35i  1671  nfn  1704  19.37aiv  1721  19.23  1724  exan  1739  equid  1747  hbae  1764  equvini  1804  equveli  1805  sbid  1820  sbieh  1836  exdistrfor  1846  dveeq2or  1862  ax11v  1873  ax11ev  1874  equs5or  1876  sb4or  1879  sb4bor  1881  nfsb2or  1883  sbequilem  1884  sbequi  1885  speiv  1908  nfsbxy  1993  nfsbxyt  1994  sbco  2019  sbcocom  2021  sbcomxyyz  2023  sbal1yz  2052  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  eumoi  2110  moani  2148  elsb1  2207  elsb2  2208  eqeq1i  2237  eqeq2i  2240  eleq1i  2295  eleq2i  2296  nfcrii  2365  neeq1i  2415  neeq2i  2416  necon3i  2448  rspec  2582  rgen2a  2584  mprg  2587  r19.21  2606  r19.23  2639  raleqi  2732  rexeqi  2733  rabeqif  2790  elv  2803  elexi  2812  ceqsal  2829  vtocl3  2857  vtoclef  2876  vtocle  2877  spcv  2897  spcev  2898  clel3  2938  elabf  2946  elab2  2951  elab3  2955  euxfrdc  2989  reueq  3002  rmoimi2  3006  sbsbc  3032  sbc8g  3036  sbc6  3054  sbcie  3063  sbcrex  3108  csbvarg  3152  csbief  3169  csbie2  3174  sbnfc2  3185  sseli  3220  sselii  3221  sseq1i  3250  sseq2i  3251  difeq1i  3318  difeq2i  3319  uneq1i  3354  uneq2i  3355  ineq1i  3401  ineq2i  3402  ssinss1  3433  difdif2ss  3461  n0ii  3500  ne0ii  3501  vn0  3502  vn0m  3503  abf  3535  disj2  3547  difid  3560  0dif  3563  disjdif  3564  difin0  3565  undif1ss  3566  difdifdirss  3576  iftruei  3608  iffalsei  3611  ifbieq2i  3626  ifbieq12i  3628  pweqi  3653  pwid  3664  sneqi  3678  elsn  3682  elpr  3687  elsn2  3700  ralsn  3709  rexsn  3710  eltp  3714  rabrsndc  3734  preq1i  3746  preq2i  3747  prid1  3772  snnz  3786  snm  3787  prnz  3790  prm  3791  tpnz  3793  snss  3803  snsssn  3839  opeq1i  3860  opeq2i  3861  unieqi  3898  unissi  3911  inteqi  3927  intmin2  3949  intab  3952  intsn  3958  iinconstm  3974  iuniin  3975  iinss1  3977  iunxdif2  4014  ssiinf  4015  iinss  4017  iinss2  4018  iinab  4027  iundif2ss  4031  iindif2m  4033  iinin2m  4034  iunxsn  4042  iunxprg  4046  iinpw  4056  invdisjrab  4077  sndisj  4079  disjxsn  4081  breqi  4089  breq1i  4090  breq2i  4091  brab1  4131  opabbii  4151  truni  4196  bm1.3ii  4205  a9evsep  4206  ax9vsep  4207  zfnuleu  4208  axnul  4209  ssexi  4222  rabex  4229  rabex2  4231  elpw2  4242  pwnss  4244  iin0r  4254  intv  4255  pwex  4268  snex  4270  notnotsnex  4272  ord3ex  4275  dtruarb  4276  undifexmid  4278  intid  4311  opnzi  4322  copsexg  4331  opwo0id  4336  opelopabf  4364  epelc  4383  elon  4466  inton  4485  onn0  4492  onm  4493  elsuc  4498  elsuc2  4499  sucid  4509  iunsuc  4512  onordi  4518  ontrci  4519  onelssi  4521  eusvnf  4545  ssonunii  4582  sucex  4592  onssi  4608  onsuci  4609  ordtriexmidlem  4612  ordtriexmidlem2  4613  ordtriexmid  4614  ontriexmidim  4615  ordtri2orexmid  4616  2ordpr  4617  ontr2exmid  4618  onsucsssucexmid  4620  onsucelsucexmid  4623  regexmidlemm  4625  reg2exmid  4629  onirri  4636  ruALT  4644  onprc  4645  sucon  4646  dtru  4653  0elsucexmid  4658  ordpwsucexmid  4663  ordtri2or2exmid  4664  ontri2orexmidim  4665  dcextest  4674  omex  4686  find  4692  omelon  4702  nnoni  4704  limom  4707  nnregexmid  4714  omsinds  4715  xpeq1i  4740  xpeq2i  4741  0nelxp  4748  opthprc  4772  mosubop  4787  releqi  4804  relssi  4812  relin1  4840  relin2  4841  reldif  4842  inopab  4857  difopab  4858  xpiindim  4862  opabbi2dv  4874  ideq  4877  coeq1i  4884  coeq2i  4885  cnveqi  4900  eldm  4923  eldm2  4924  dmeqi  4927  dmv  4942  rneqi  4955  elrnmpti  4980  dmex  4994  rnex  4995  reseq1i  5004  reseq2i  5005  residm  5040  resex  5049  resmpt3  5057  imaeq1i  5068  imaeq2i  5069  elima  5076  imaex  5086  elimasn  5098  args  5100  epini  5102  dfse2  5104  eliniseg2  5111  relbrcnv  5112  cotr  5113  issref  5114  cnvsym  5115  asymref  5117  intirr  5118  codir  5120  qfto  5121  ssrnres  5174  cnveq0  5188  cnvsn0  5200  dmsnop  5205  rnsnop  5212  resdm2  5222  dfco2a  5232  cocnvcnv1  5242  coi2  5248  coires1  5249  cnvssrndm  5253  cossxp  5254  cocnvres  5256  relrelss  5258  relcoi2  5262  unidmrn  5264  dfdm2  5266  unixpm  5267  cnvexg  5269  cnvex  5270  cnviinm  5273  iotaval  5293  funeqi  5342  funi  5353  funres  5362  funcnvsn  5369  funcnvcnv  5383  funin  5395  funcnvres  5397  isarep2  5411  fneq1i  5418  fneq2i  5419  fndmi  5424  fnresdisj  5436  fnresi  5444  mpt0  5454  dmmpti  5456  feq1i  5469  feq2i  5470  fdmi  5484  fun2  5503  fssres  5506  resasplitss  5510  fintm  5516  fconst6  5530  f1ores  5592  foimacnv  5595  resdif  5599  funcocnv2  5602  f10d  5612  f1ovi  5617  fveq1i  5633  fveq2i  5635  0fv  5670  fvun1  5705  fvopab3ig  5713  fvmptss2  5714  mptrcl  5722  elfvmptrab1  5734  fndmdif  5745  fneqeql2  5749  f1oresrab  5805  fmptco  5806  funopsn  5822  fnressn  5832  fressnfv  5833  fmptap  5836  fvsnun1  5843  fvsnun2  5844  fsnunfv  5847  fconst2  5863  mptex  5872  fnfvimad  5882  riotabiia  5982  acexmidlema  6001  acexmidlemb  6002  acexmidlemcase  6005  acexmidlem2  6007  acexmidlemv  6008  oveq1i  6020  oveq2i  6021  oveqi  6023  oprabidlem  6041  0neqopab  6058  oprabbii  6068  oprabss  6099  mpompt  6105  funoprab  6113  fnoprab  6116  ovigg  6134  elmpocl  6209  relmptopab  6216  resfunexgALT  6262  cofunexg  6263  mptexw  6267  opabex3d  6275  opabex3  6276  1st0  6299  2nd0  6300  op1st  6301  op2nd  6302  f1stres  6314  f2ndres  6315  fo1stresm  6316  fo2ndresm  6317  1stcof  6318  2ndcof  6319  1stexg  6322  2ndexg  6323  releldm2  6340  reldm  6341  dfoprab3  6346  mpomptsx  6354  mpompts  6355  fnmpoi  6360  dmmpo  6361  mpoexxg  6367  mpoexw  6370  1stconst  6378  2ndconst  6379  dfmpo  6380  algrflem  6386  algrflemg  6387  cnvoprab  6391  f1od2  6392  mpoxopn0yelv  6396  mpoxopoveq  6397  tposssxp  6406  brtpos2  6408  reldmtpos  6410  dftpos2  6418  dftpos4  6420  tpostpos  6421  tpostpos2  6422  tposfo  6428  tposf  6429  tposeqi  6434  tposex  6435  tposoprab  6437  issmo  6445  smores  6449  smores2  6451  iordsmo  6454  smo0  6455  tfrlem8  6475  tfrexlem  6491  tfr1onlem3  6495  tfr1onlemsucaccv  6498  tfr1onlembxssdm  6500  tfr1onlemres  6506  tfri1dALT  6508  tfri2  6523  rdgisuc1  6541  rdg0  6544  frecfun  6552  frec0g  6554  freccllem  6559  frecfcllem  6561  frecsuclem  6563  frecrdg  6565  2on0  6583  xp01disj  6592  2oconcl  6598  fnoa  6606  oaexg  6607  fnom  6609  omexg  6610  fnoei  6611  oeiexg  6612  oei0  6618  oacl  6619  oasuc  6623  o1p1e2  6627  omsuc  6631  nna0r  6637  nnm0r  6638  1onn  6679  2onn  6680  3onn  6681  4onn  6682  2ssom  6683  eqerlem  6724  eceq2i  6731  elqs  6746  qsex  6752  ecqs  6757  iinerm  6767  th3qlem1  6797  th3q  6800  mapsn  6850  mapsnf1o3  6857  ixpiinm  6884  ixpssmap  6892  brdom  6912  f1dom  6924  enref  6929  dom2  6939  idssen  6941  ssdomg  6943  ensymi  6947  ensn1  6961  fiprc  6981  1domsn  6989  dom1o  6990  xpcomf1o  6997  xpcomco  6998  dom0  7012  0dom  7013  xpmapenlem  7023  phplem2  7027  php5  7032  snnen2og  7033  1nen2  7035  php5dom  7037  ssfilem  7050  ssfiexmid  7051  domfiexmid  7053  0fi  7059  diffitest  7062  findcard  7063  findcard2  7064  findcard2s  7065  isinfinf  7072  ac6sfi  7073  inffiexmid  7084  pw1fin  7088  unfiexmid  7096  xpfi  7110  fisseneq  7112  ssfirab  7114  residfi  7123  en1eqsn  7131  snexxph  7133  sbthlem2  7141  sbthlemi3  7142  sbthlemi6  7145  sbthlem7  7146  fi0  7158  supeq1i  7171  infeq1i  7196  djuexb  7227  djuf1olemr  7237  inresflem  7243  djuinr  7246  updjudhcoinlf  7263  updjudhcoinrg  7264  casefun  7268  caserel  7270  caseinj  7272  caseinl  7274  caseinr  7275  omp1eomlem  7277  endjusym  7279  difinfsn  7283  difinfinf  7284  djuinj  7289  0ct  7290  ctmlemr  7291  ctssdclemn0  7293  ctssdccl  7294  omct  7300  ctfoex  7301  finomni  7323  exmidomni  7325  fodjuomni  7332  ctssexmid  7333  fodjumkv  7343  nninfwlporlem  7356  nninfwlpoimlemg  7358  nninfwlpoim  7362  nninfinfwlpo  7363  card0  7376  ficardon  7377  exmidonfinlem  7387  dju1p1e2  7391  exmidfodomrlemim  7395  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  iftrueb01  7424  3nelsucpw1  7435  sucpw1nss3  7436  3nsssucpw1  7437  2onetap  7457  exmidmotap  7463  0npi  7516  dmaddpi  7528  dmmulpi  7529  1lt2pi  7543  0nnq  7567  1nq  7569  dmaddpq  7582  dmmulpq  7583  rec1nq  7598  1lt2nq  7609  halfnqq  7613  prarloclemarch2  7622  enq0enq  7634  nqnq0pi  7641  nnnq0lem1  7649  addnnnq0  7652  mulnnnq0  7653  nq0m0r  7659  addpinq1  7667  prarloclem5  7703  prarloclemcalc  7705  1pr  7757  1idprl  7793  1idpru  7794  ltexprlemm  7803  recexprlem1ssl  7836  recexprlem1ssu  7837  suplocexprlemell  7916  suplocexprlem2b  7917  suplocexprlemmu  7921  suplocexprlemdisj  7923  suplocexprlemloc  7924  suplocexprlemub  7926  suplocexprlemlub  7927  prsrlem1  7945  addsrpr  7948  mulsrpr  7949  gt0srpr  7951  0nsr  7952  0r  7953  1sr  7954  m1r  7955  m1m1sr  7964  caucvgsr  8005  suplocsrlempr  8010  addresr  8040  mulresr  8041  pitonnlem1  8048  peano1nnnn  8055  axi2m1  8078  axcnre  8084  peano5nnnn  8095  axcaucvg  8103  mpomulf  8152  mulridi  8164  mullidi  8165  pnfnre  8204  mnfnre  8205  pnfnemnf  8217  mnfxr  8219  rexri  8220  ltnri  8255  ltleii  8265  00id  8303  addridi  8304  addlidi  8305  0cnALT  8352  negeqi  8356  negicn  8363  neg0  8408  renegcli  8424  negcli  8430  negidi  8431  negnegi  8432  subidi  8433  subid1i  8434  negne0bi  8435  negrebi  8436  mul02i  8552  mul01i  8553  mulm1i  8565  leidi  8648  gt0ne0ii  8650  inelr  8747  msqge0i  8780  gt0ap0ii  8791  1div1e1  8867  div1i  8903  eqnegi  8904  recclapi  8905  recidapi  8906  divmulapi  8929  rerecclapi  8940  redivclapi  8942  rerecapb  9006  recgt0  9013  ltp1i  9068  divgt0ii  9082  ltmul1ii  9091  ltdiv1ii  9092  sup3exmid  9120  peano5nni  9129  nnrei  9135  1nn  9137  nngt0i  9156  neg1ap0  9235  2timesi  9256  times2i  9257  2nn  9288  3nn  9289  4nn  9290  5nn  9291  6nn  9292  7nn  9293  8nn  9294  9nn  9295  2muline0  9352  rehalfcli  9376  nn0ssre  9389  nnnn0i  9393  dfn2  9398  0nn0  9400  nn0ge0i  9412  zrei  9468  neg1z  9494  nn0negzi  9497  dfz2  9535  nneoi  9567  peano5uzi  9572  dfuzi  9573  nn0ind-raph  9580  deceq1i  9600  deceq2i  9601  10nn  9609  numltc  9619  eluzel2  9743  eluz1i  9746  nn0uz  9774  nnuz  9775  infrenegsupex  9806  lbzbi  9828  divfnzn  9833  qdivcl  9855  irrmul  9859  irrmulap  9860  cnref1o  9863  0ltpnf  9995  mnflt0  9997  0lepnf  10003  xrltnsym  10006  xrlttri3  10010  nltpnft  10027  ngtmnft  10030  xrrebnd  10032  xnegmnf  10042  xneg0  10044  xltnegi  10048  xaddmnf1  10061  xaddmnf2  10062  mnfaddpnf  10064  xaddid1  10075  xnn0lenn0nn0  10078  xnn0xadd0  10080  xposdif  10095  ixxex  10112  iooval2  10128  unirnioo  10186  ioorebasg  10188  elrege0  10189  fzval2  10224  fzen  10256  fzprval  10295  fztpval  10296  uzdisj  10306  ige2m1fz  10323  fz01or  10324  fz1ssfz0  10330  fz0sn  10334  fz0tp  10335  fz0to3un2pr  10336  fz0to4untppr  10337  nn0disj  10351  1fv  10352  4fvwrd4  10353  fzo0ss1  10389  fzo01  10439  fzo12sn  10440  fzo0to2pr  10441  fzo0to3tp  10442  fzo0to42pr  10443  zsupssdc  10475  qbtwnxr  10494  flval  10509  fldiv4lem1div2  10544  modqfrac  10576  modqmulnn  10581  q2txmodxeq0  10623  frecuzrdgdom  10657  frecuzrdgfun  10659  frecuzrdgsuct  10663  frechashgf1o  10667  nnct  10674  xnn0nnen  10676  fxnn0nninf  10678  0tonninf  10679  1tonninf  10680  iseqvalcbv  10698  ser0f  10773  0exp0e1  10783  qexpcl  10794  qexpclz  10799  m1expcl2  10800  1exp  10807  sqvali  10858  sqcli  10859  sqeq0i  10860  resqcli  10863  sq1  10872  neg1sqe1  10873  iexpcyc  10883  qsqeqor  10889  facnn  10966  fac0  10967  fac1  10968  fac2  10970  fac3  10971  fac4  10972  bcval  10988  bcm1k  10999  bcpasc  11005  bccl  11006  4bc3eq4  11012  4bc2eq6  11013  hashinfom  11017  hashennn  11019  hashfz1  11022  fihasheq0  11032  hash0  11035  hashsng  11037  fihashen1  11038  omgadd  11041  hashp1i  11050  hashxp  11066  fimaxq  11067  zfz1iso  11081  hash2en  11083  wrdexi  11102  wrdv  11105  wrdeqi  11112  wrd0  11114  lsw0  11137  ccatclab  11147  ccatidid  11163  s1prc  11176  ccat1st1st  11193  swrds1  11221  fnpfx  11230  swrdccatin2  11282  pfxccatin12lem2  11284  cats1fvn  11317  shftidt2  11364  cjexp  11425  re0  11427  im0  11428  re1  11429  im1  11430  cj0  11433  cji  11434  recli  11443  imcli  11444  cjcli  11445  replimi  11446  cjcji  11447  reim0bi  11448  rerebi  11449  cjrebi  11450  recji  11451  imcji  11452  cjmulrcli  11453  cjmulvali  11454  cjmulge0i  11455  renegi  11456  imnegi  11457  cjnegi  11458  addcji  11459  uzin2  11519  rexanuz  11520  rexfiuz  11521  sqrtrval  11532  sqrt0  11536  resqrexlemcalc3  11548  resqrexlemcvg  11551  resqrex  11558  abs0  11590  absi  11591  qabsor  11607  absimle  11616  recan  11641  caubnd2  11649  leabsi  11660  absrei  11661  sqrtpclii  11662  sqrtgt0ii  11663  absvalsqi  11672  absvalsq2i  11673  abscli  11674  absge0i  11675  absval2i  11676  abs00i  11677  absgt0api  11678  absnegi  11679  abscji  11680  releabsi  11681  infxrnegsupex  11795  xrbdtri  11808  cbvsum  11892  sumeq1i  11895  sum0  11920  isumz  11921  fisumss  11924  fsumsersdc  11927  fsumadd  11938  isumclim  11953  isumclim3  11955  fsumcnv  11969  modfsummodlem1  11988  fsumrelem  12003  binomlem  12015  binom  12016  arisum2  12031  expcnv  12036  0.999...  12053  prodf1f  12075  cbvprod  12090  prodeq1i  12093  zproddc  12111  zprodap0  12113  prod0  12117  fprodssdc  12122  prodsnf  12124  fprodcnv  12157  fprodge0  12169  fprodge1  12171  ef0lem  12192  esum  12194  ere  12202  ege2le3  12203  ef0  12204  eff2  12212  efsep  12223  reeff1  12232  sin0  12261  cos0  12262  ef01bndlem  12288  cos2bnd  12292  sincos1sgn  12297  sincos2sgn  12298  sin4lt0  12299  eirr  12311  0dvds  12343  dvds1  12385  z0even  12443  n2dvdsm1  12445  z2even  12446  n2dvds3  12447  ndvdssub  12462  ndvdsi  12465  flodddiv4  12468  bits0  12480  bitsfzo  12487  0bits  12491  m1bits  12492  bitsinv1lem  12493  bitsinv1  12494  gcddvds  12505  gcd1  12529  6gcd4e2  12537  bezoutlembi  12547  dfgcd3  12552  dfgcd2  12556  nninfctlemfo  12582  nninfct  12583  3lcm2e6woprm  12629  qredeu  12640  isprm2lem  12659  isprm3  12661  prm2orodd  12669  isprm5lem  12684  sqrt2irr0  12707  pw2dvds  12709  phicl2  12757  phi1  12762  dfphi2  12763  phiprmpw  12765  eulerthlemrprm  12772  eulerthlemh  12774  odzval  12785  oddprm  12803  pczpre  12841  pcdiv  12846  pc0  12848  pcqdiv  12851  pcrec  12852  pcexp  12853  pcxcl  12855  pcxqcl  12856  pcdvdstr  12871  pc2dvds  12874  dvdsprmpweqnn  12880  pcmpt  12887  qexpz  12896  pockthi  12902  1arith2  12912  4sqlemffi  12940  4sqlem11  12945  4sqlem13m  12947  4sqlem19  12953  dec2dvds  12955  dec5nprm  12958  modxai  12960  modxp1i  12962  numexp0  12966  numexp1  12967  ennnfonelemp1  12998  ennnfonelem1  12999  ennnfonelemkh  13004  ennnfonelemex  13006  ennnfonelemnn0  13014  ennnfonelemr  13015  exmidunben  13018  ctinfomlemom  13019  ctinfom  13020  ctinf  13022  qnnen  13023  omctfn  13035  omiunct  13036  ssnnctlemct  13038  nninfdc  13045  structcnvcnv  13069  structfun  13071  structfn  13072  ndxarg  13076  ndxid  13077  setsresg  13091  setsslnid  13105  basmex  13113  basmexd  13114  strleun  13158  strle1g  13160  prdsex  13323  prdsvallem  13326  prdsval  13327  prdsbaslemss  13328  imasaddfnlemg  13368  quslem  13378  xpsfrnel  13398  xpsff1o  13403  ismgmn0  13412  fn0g  13429  0g0  13430  fngsum  13442  idghm  13817  rhmfn  14157  rmodislmodlem  14335  rmodislmod  14336  lidlmex  14460  mopnset  14537  cntopex  14539  cnfldex  14544  cnfldbas  14545  mpocnfldadd  14546  mpocnfldmul  14548  cnfldcj  14550  cnfldtset  14551  cnfldle  14552  cnfldds  14553  cnring  14555  cnfld0  14556  cnfld1  14557  cnfldneg  14558  cnfldplusf  14559  cnfldsub  14560  cnfldmulg  14561  cnfldexp  14562  cnsubglem  14564  cnsubrglem  14565  gzsubrg  14567  gsumfzfsumlem0  14571  cnfldui  14574  zringring  14578  zringabl  14579  zringgrp  14580  zring1  14586  zringsubgval  14590  expghmap  14592  znval  14621  znle  14622  znbaslemnn  14624  znbas  14629  znzrh2  14631  znzrhval  14632  znzrhfo  14633  znleval  14638  znidom  14642  znidomb  14643  fnpsr  14652  psrelbas  14660  psradd  14664  psraddcl  14665  psr1clfi  14673  mplrcl  14679  mplbasss  14681  mpladd  14689  istopon  14708  topontopi  14711  toponunii  14712  toponrestid  14716  istps  14727  topontopn  14732  eltpsi  14736  eltg4i  14750  eltg3  14752  tg1  14754  tg2  14755  tgclb  14760  topnex  14781  sn0topon  14783  distps  14786  cldrcl  14797  sn0cld  14832  restco  14869  lmrcl  14887  ssidcn  14905  cnconst2  14928  cnptopresti  14933  cnptoprest  14934  txuni2  14951  txbas  14953  eltx  14954  txcnp  14966  upxp  14967  txcnmpt  14968  uptx  14969  txcn  14970  txrest  14971  txlm  14974  cnmptid  14976  cnmpt1st  14983  cnmpt2nd  14984  hmeofn  14997  psmetge0  15026  ismeti  15041  xmetunirn  15053  xmetge0  15060  unirnblps  15117  unirnbl  15118  mopnex  15200  qtopbasss  15216  retop  15219  uniretop  15220  iooretopg  15223  cnxmet  15226  cntoptopon  15227  cnbl0  15229  cnfldxms  15232  cnfldtps  15233  rexmet  15244  blssioo  15248  tgioo  15249  tgqioo  15250  cnopnap  15306  hovercncf  15341  limcresi  15361  dvfvalap  15376  dvidlemap  15386  dvidrelem  15387  dvidsslem  15388  dvcnp2cntop  15394  dvcoapbr  15402  dvexp2  15407  dvrecap  15408  dveflem  15421  dvef  15422  plyun0  15431  plyrecj  15458  dvply2  15462  reeff1o  15468  sin0pilem1  15476  sin0pilem2  15477  pilem3  15478  pigt2lt4  15479  pire  15481  sinhalfpilem  15486  pidiv2halves  15490  cosneghalfpi  15493  cospi  15495  efipi  15496  sin2pi  15498  cos2pi  15499  ef2pi  15500  cosq14gt0  15527  coseq00topi  15530  coseq0negpitopi  15531  sincos4thpi  15535  sincos6thpi  15537  sincos3rdpi  15538  pigt3  15539  cos02pilt1  15546  ioocosf1o  15549  dfrelog  15555  relogf1o  15556  relogcl  15557  relogiso  15568  rpcxpsqrt  15617  rpabscxpbnd  15635  2logb9irr  15666  2logb9irrALT  15669  sqrt2cxp2logb9e3  15670  2irrexpq  15671  2logb9irrap  15672  2irrexpqap  15673  mpodvdsmulf1o  15685  fsumdvdsmul  15686  perfectlem2  15695  lgsdir2lem1  15728  lgsdir2lem2  15729  lgsdir2lem4  15731  lgsdir2lem5  15732  lgsdi  15737  gausslemma2dlem0i  15757  gausslemma2dlem4  15764  lgseisenlem4  15773  lgsquadlem1  15777  lgsquad2lem2  15782  lgsquad2  15783  m1lgs  15785  2lgs2  15802  2lgslem4  15803  2lgsoddprmlem2  15806  2lgsoddprmlem3c  15809  2lgsoddprmlem3d  15810  2sqlem9  15824  2sqlem10  15825  1vgrex  15842  vtxval0  15875  iedgval0  15876  uhgr0  15906  upgrfi  15923  umgrislfupgrdom  15950  ausgrusgrben  15987  uspgredgiedg  15997  uspgriedgedg  15998  usgrislfuspgrdom  16009  uspgredg2vlem  16039  uspgredg2v  16040  usgr0  16058  griedg0prc  16069  0wlk0  16143  clwwlkn1  16186  clwwlkn2  16189  ex-fl  16198  ex-ceil  16199  ex-exp  16200  ex-fac  16201  ex-gcd  16204  bj-stfal  16215  bj-stst  16218  bj-dcfal  16228  bj-dcdc  16232  bj-stdc  16233  bj-dcst  16234  bj-el2oss1o  16247  elabf2  16255  bd0  16296  bdeli  16318  bdcriota  16355  bdbm1.3ii  16363  bdinex1  16371  bdssexi  16375  bj-inex  16379  bj-snex  16385  bj-sucex  16395  bj-d0clsepcl  16397  bj-omind  16406  bj-om  16409  bj-2inf  16410  bj-peano2  16411  bdpeano5  16415  bj-omssonALT  16435  bj-inf2vnlem1  16442  bj-omex2  16449  bj-nn0sucALT  16450  3dom  16465  012of  16470  2o01f  16471  subctctexmid  16479  pw1dceq  16483  nninfall  16489  nninfsellemqall  16495  nninfsellemeqinf  16496  nninfomnilem  16498  nninfomni  16499  exmidsbthrlem  16504  sbthom  16508  isomninnlem  16512  isomninn  16513  cvgcmp2nlemabs  16514  iooreen  16517  trilpolemisumle  16520  trilpolemeq1  16522  trilpo  16525  trirec0  16526  apdifflemr  16529  iswomninnlem  16531  iswomninn  16532  ismkvnnlem  16534  ismkvnn  16535  redcwlpo  16537  dcapnconst  16543  nconstwlpolem0  16545  nconstwlpo  16548  neapmkv  16550  neap0mkv  16551  taupi  16555