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

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  644  notnoti  650  pm2.21i  651  pm2.24ii  652  notbii  674  nbn  706  ori  730  orci  738  olci  739  biorfi  753  imorri  756  dcbii  847  simp1i  1032  simp2i  1033  simp3i  1034  3mix1i  1195  3mix2i  1196  3mix3i  1197  3jaoi  1339  mptru  1406  dfnot  1415  mptnan  1467  mtpor  1469  mtpxor  1470  dcfromnotnotr  1492  dcfromcon  1493  dcfrompeirce  1494  mpg  1499  19.23h  1546  hbequid  1561  axi12  1562  nfri  1567  spi  1584  19.21  1631  eximii  1650  19.35i  1673  nfn  1706  19.37aiv  1723  19.23  1726  exan  1741  equid  1749  hbae  1766  equvini  1806  equveli  1807  sbid  1822  sbieh  1838  exdistrfor  1848  dveeq2or  1864  ax11v  1875  ax11ev  1876  equs5or  1878  sb4or  1881  sb4bor  1883  nfsb2or  1885  sbequilem  1886  sbequi  1887  speiv  1910  nfsbxy  1995  nfsbxyt  1996  sbco  2021  sbcocom  2023  sbcomxyyz  2025  sbal1yz  2054  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  eumoi  2112  moani  2150  elsb1  2209  elsb2  2210  eqeq1i  2239  eqeq2i  2242  eleq1i  2297  eleq2i  2298  nfcrii  2367  neeq1i  2417  neeq2i  2418  necon3i  2450  rspec  2584  rgen2a  2586  mprg  2589  r19.21  2608  r19.23  2641  raleqi  2734  rexeqi  2735  rabeqif  2793  elv  2806  elexi  2815  ceqsal  2832  vtocl3  2860  vtoclef  2879  vtocle  2880  spcv  2900  spcev  2901  clel3  2941  elabf  2949  elab2  2954  elab3  2958  euxfrdc  2992  reueq  3005  rmoimi2  3009  sbsbc  3035  sbc8g  3039  sbc6  3057  sbcie  3066  sbcrex  3111  csbvarg  3155  csbief  3172  csbie2  3177  sbnfc2  3188  sseli  3223  sselii  3224  sseq1i  3253  sseq2i  3254  difeq1i  3321  difeq2i  3322  uneq1i  3357  uneq2i  3358  ineq1i  3404  ineq2i  3405  ssinss1  3436  difdif2ss  3464  n0ii  3503  ne0ii  3504  vn0  3505  vn0m  3506  abf  3538  disj2  3550  difid  3563  0dif  3566  disjdif  3567  difin0  3568  undif1ss  3569  difdifdirss  3579  iftruei  3611  iffalsei  3614  ifbieq2i  3629  ifbieq12i  3631  pweqi  3656  pwid  3667  sneqi  3681  elsn  3685  elpr  3690  elsn2  3703  ralsn  3712  rexsn  3713  eltp  3717  rabrsndc  3739  preq1i  3751  preq2i  3752  prid1  3777  snnz  3791  snm  3792  prnz  3795  prm  3796  tpnz  3798  snss  3808  snsssn  3844  opeq1i  3865  opeq2i  3866  unieqi  3903  unissi  3916  inteqi  3932  intmin2  3954  intab  3957  intsn  3963  iinconstm  3979  iuniin  3980  iinss1  3982  iunxdif2  4019  ssiinf  4020  iinss  4022  iinss2  4023  iinab  4032  iundif2ss  4036  iindif2m  4038  iinin2m  4039  iunxsn  4047  iunxprg  4051  iinpw  4061  invdisjrab  4082  sndisj  4084  disjxsn  4086  breqi  4094  breq1i  4095  breq2i  4096  brab1  4136  opabbii  4156  truni  4201  bm1.3ii  4210  a9evsep  4211  ax9vsep  4212  zfnuleu  4213  axnul  4214  ssexi  4227  rabex  4234  rabex2  4236  elpw2  4247  pwnss  4249  iin0r  4259  intv  4260  pwex  4273  snex  4275  notnotsnex  4277  ord3ex  4280  dtruarb  4281  undifexmid  4283  intid  4316  opnzi  4327  copsexg  4336  opwo0id  4341  opelopabf  4369  epelc  4388  elon  4471  inton  4490  onn0  4497  onm  4498  elsuc  4503  elsuc2  4504  sucid  4514  iunsuc  4517  onordi  4523  ontrci  4524  onelssi  4526  eusvnf  4550  ssonunii  4587  sucex  4597  onssi  4613  onsuci  4614  ordtriexmidlem  4617  ordtriexmidlem2  4618  ordtriexmid  4619  ontriexmidim  4620  ordtri2orexmid  4621  2ordpr  4622  ontr2exmid  4623  onsucsssucexmid  4625  onsucelsucexmid  4628  regexmidlemm  4630  reg2exmid  4634  onirri  4641  ruALT  4649  onprc  4650  sucon  4651  dtru  4658  0elsucexmid  4663  ordpwsucexmid  4668  ordtri2or2exmid  4669  ontri2orexmidim  4670  dcextest  4679  omex  4691  find  4697  omelon  4707  nnoni  4709  limom  4712  nnregexmid  4719  omsinds  4720  xpeq1i  4745  xpeq2i  4746  0nelxp  4753  opthprc  4777  mosubop  4792  releqi  4809  relssi  4817  relin1  4845  relin2  4846  reldif  4847  inopab  4862  difopab  4863  xpiindim  4867  opabbi2dv  4879  ideq  4882  coeq1i  4889  coeq2i  4890  cnveqi  4905  eldm  4928  eldm2  4929  dmeqi  4932  dmv  4947  rneqi  4960  elrnmpti  4985  dmex  4999  rnex  5000  reseq1i  5009  reseq2i  5010  residm  5045  resex  5054  resmpt3  5062  imaeq1i  5073  imaeq2i  5074  elima  5081  imaex  5091  elimasn  5103  args  5105  epini  5107  dfse2  5109  eliniseg2  5116  relbrcnv  5117  cotr  5118  issref  5119  cnvsym  5120  asymref  5122  intirr  5123  codir  5125  qfto  5126  ssrnres  5179  cnveq0  5193  cnvsn0  5205  dmsnop  5210  rnsnop  5217  resdm2  5227  dfco2a  5237  cocnvcnv1  5247  coi2  5253  coires1  5254  cnvssrndm  5258  cossxp  5259  cocnvres  5261  relrelss  5263  relcoi2  5267  unidmrn  5269  dfdm2  5271  unixpm  5272  cnvexg  5274  cnvex  5275  cnviinm  5278  iotaval  5298  funeqi  5347  funi  5358  funres  5367  funcnvsn  5375  funcnvcnv  5389  funin  5401  funcnvres  5403  isarep2  5417  fneq1i  5424  fneq2i  5425  fndmi  5430  fnresdisj  5442  fnresi  5450  mpt0  5460  dmmpti  5462  feq1i  5475  feq2i  5476  fdmi  5490  fun2  5509  fssres  5512  resasplitss  5516  fintm  5522  fconst6  5536  f1ores  5598  foimacnv  5601  resdif  5605  funcocnv2  5608  f10d  5619  f1ovi  5624  fveq1i  5640  fveq2i  5642  0fv  5677  fvun1  5712  fvopab3ig  5720  fvmptss2  5721  mptrcl  5729  elfvmptrab1  5741  fndmdif  5752  fneqeql2  5756  f1oresrab  5812  fmptco  5813  funopsn  5829  fnressn  5839  fressnfv  5840  fmptap  5843  fvsnun1  5850  fvsnun2  5851  fsnunfv  5854  fconst2  5870  mptex  5879  fnfvimad  5889  riotabiia  5989  acexmidlema  6008  acexmidlemb  6009  acexmidlemcase  6012  acexmidlem2  6014  acexmidlemv  6015  oveq1i  6027  oveq2i  6028  oveqi  6030  oprabidlem  6048  0neqopab  6065  oprabbii  6075  oprabss  6106  mpompt  6112  funoprab  6120  fnoprab  6123  ovigg  6141  elmpocl  6216  relmptopab  6223  resfunexgALT  6269  cofunexg  6270  mptexw  6274  opabex3d  6282  opabex3  6283  1st0  6306  2nd0  6307  op1st  6308  op2nd  6309  f1stres  6321  f2ndres  6322  fo1stresm  6323  fo2ndresm  6324  1stcof  6325  2ndcof  6326  1stexg  6329  2ndexg  6330  releldm2  6347  reldm  6348  dfoprab3  6353  mpomptsx  6361  mpompts  6362  fnmpoi  6367  dmmpo  6368  mpoexxg  6374  mpoexw  6377  1stconst  6385  2ndconst  6386  dfmpo  6387  algrflem  6393  algrflemg  6394  cnvoprab  6398  f1od2  6399  elmpom  6402  mpoxopn0yelv  6404  mpoxopoveq  6405  tposssxp  6414  brtpos2  6416  reldmtpos  6418  dftpos2  6426  dftpos4  6428  tpostpos  6429  tpostpos2  6430  tposfo  6436  tposf  6437  tposeqi  6442  tposex  6443  tposoprab  6445  issmo  6453  smores  6457  smores2  6459  iordsmo  6462  smo0  6463  tfrlem8  6483  tfrexlem  6499  tfr1onlem3  6503  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlemres  6514  tfri1dALT  6516  tfri2  6531  rdgisuc1  6549  rdg0  6552  frecfun  6560  frec0g  6562  freccllem  6567  frecfcllem  6569  frecsuclem  6571  frecrdg  6573  2on0  6591  xp01disj  6600  2oconcl  6606  fnoa  6614  oaexg  6615  fnom  6617  omexg  6618  fnoei  6619  oeiexg  6620  oei0  6626  oacl  6627  oasuc  6631  o1p1e2  6635  omsuc  6639  nna0r  6645  nnm0r  6646  1onn  6687  2onn  6688  3onn  6689  4onn  6690  2ssom  6691  eqerlem  6732  eceq2i  6739  elqs  6754  qsex  6760  ecqs  6765  iinerm  6775  th3qlem1  6805  th3q  6808  mapsn  6858  mapsnf1o3  6865  ixpiinm  6892  ixpssmap  6900  brdom  6920  f1dom  6932  enref  6937  dom2  6947  idssen  6949  ssdomg  6951  ensymi  6955  ensn1  6969  fiprc  6989  1domsn  7000  dom1o  7001  xpcomf1o  7008  xpcomco  7009  dom0  7023  0dom  7024  xpmapenlem  7034  phplem2  7038  php5  7043  snnen2og  7044  1nen2  7046  php5dom  7048  ssfilem  7061  ssfiexmid  7062  ssfilemd  7063  ssfiexmidt  7064  domfiexmid  7066  0fi  7072  diffitest  7075  findcard  7076  findcard2  7077  findcard2s  7078  isinfinf  7085  ac6sfi  7086  inffiexmid  7097  pw1fin  7101  unfiexmid  7109  xpfi  7123  fisseneq  7126  ssfirab  7128  residfi  7138  en1eqsn  7146  snexxph  7148  sbthlem2  7156  sbthlemi3  7157  sbthlemi6  7160  sbthlem7  7161  fi0  7173  supeq1i  7186  infeq1i  7211  djuexb  7242  djuf1olemr  7252  inresflem  7258  djuinr  7261  updjudhcoinlf  7278  updjudhcoinrg  7279  casefun  7283  caserel  7285  caseinj  7287  caseinl  7289  caseinr  7290  omp1eomlem  7292  endjusym  7294  difinfsn  7298  difinfinf  7299  djuinj  7304  0ct  7305  ctmlemr  7306  ctssdclemn0  7308  ctssdccl  7309  omct  7315  ctfoex  7316  finomni  7338  exmidomni  7340  fodjuomni  7347  ctssexmid  7348  fodjumkv  7358  nninfwlporlem  7371  nninfwlpoimlemg  7373  nninfwlpoim  7377  nninfinfwlpo  7378  card0  7391  ficardon  7392  exmidonfinlem  7403  dju1p1e2  7407  exmidfodomrlemim  7411  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  iftrueb01  7440  3nelsucpw1  7451  sucpw1nss3  7452  3nsssucpw1  7453  2onetap  7473  exmidmotap  7479  0npi  7532  dmaddpi  7544  dmmulpi  7545  1lt2pi  7559  0nnq  7583  1nq  7585  dmaddpq  7598  dmmulpq  7599  rec1nq  7614  1lt2nq  7625  halfnqq  7629  prarloclemarch2  7638  enq0enq  7650  nqnq0pi  7657  nnnq0lem1  7665  addnnnq0  7668  mulnnnq0  7669  nq0m0r  7675  addpinq1  7683  prarloclem5  7719  prarloclemcalc  7721  1pr  7773  1idprl  7809  1idpru  7810  ltexprlemm  7819  recexprlem1ssl  7852  recexprlem1ssu  7853  suplocexprlemell  7932  suplocexprlem2b  7933  suplocexprlemmu  7937  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemub  7942  suplocexprlemlub  7943  prsrlem1  7961  addsrpr  7964  mulsrpr  7965  gt0srpr  7967  0nsr  7968  0r  7969  1sr  7970  m1r  7971  m1m1sr  7980  caucvgsr  8021  suplocsrlempr  8026  addresr  8056  mulresr  8057  pitonnlem1  8064  peano1nnnn  8071  axi2m1  8094  axcnre  8100  peano5nnnn  8111  axcaucvg  8119  mpomulf  8168  mulridi  8180  mullidi  8181  pnfnre  8220  mnfnre  8221  pnfnemnf  8233  mnfxr  8235  rexri  8236  ltnri  8271  ltleii  8281  00id  8319  addridi  8320  addlidi  8321  0cnALT  8368  negeqi  8372  negicn  8379  neg0  8424  renegcli  8440  negcli  8446  negidi  8447  negnegi  8448  subidi  8449  subid1i  8450  negne0bi  8451  negrebi  8452  mul02i  8568  mul01i  8569  mulm1i  8581  leidi  8664  gt0ne0ii  8666  inelr  8763  msqge0i  8796  gt0ap0ii  8807  1div1e1  8883  div1i  8919  eqnegi  8920  recclapi  8921  recidapi  8922  divmulapi  8945  rerecclapi  8956  redivclapi  8958  rerecapb  9022  recgt0  9029  ltp1i  9084  divgt0ii  9098  ltmul1ii  9107  ltdiv1ii  9108  sup3exmid  9136  peano5nni  9145  nnrei  9151  1nn  9153  nngt0i  9172  neg1ap0  9251  2timesi  9272  times2i  9273  2nn  9304  3nn  9305  4nn  9306  5nn  9307  6nn  9308  7nn  9309  8nn  9310  9nn  9311  2muline0  9368  rehalfcli  9392  nn0ssre  9405  nnnn0i  9409  dfn2  9414  0nn0  9416  nn0ge0i  9428  zrei  9484  neg1z  9510  nn0negzi  9513  dfz2  9551  nneoi  9583  peano5uzi  9588  dfuzi  9589  nn0ind-raph  9596  deceq1i  9616  deceq2i  9617  10nn  9625  numltc  9635  eluzel2  9759  eluz1i  9762  nn0uz  9790  nnuz  9791  uzuzle35  9798  infrenegsupex  9827  lbzbi  9849  divfnzn  9854  qdivcl  9876  irrmul  9880  irrmulap  9881  cnref1o  9884  0ltpnf  10016  mnflt0  10018  0lepnf  10024  xrltnsym  10027  xrlttri3  10031  nltpnft  10048  ngtmnft  10051  xrrebnd  10053  xnegmnf  10063  xneg0  10065  xltnegi  10069  xaddmnf1  10082  xaddmnf2  10083  mnfaddpnf  10085  xaddid1  10096  xnn0lenn0nn0  10099  xnn0xadd0  10101  xposdif  10116  ixxex  10133  iooval2  10149  unirnioo  10207  ioorebasg  10209  elrege0  10210  fzval2  10245  fzen  10277  fzprval  10316  fztpval  10317  uzdisj  10327  ige2m1fz  10344  fz01or  10345  fz1ssfz0  10351  fz0sn  10355  fz0tp  10356  fz0to3un2pr  10357  fz0to4untppr  10358  nn0disj  10372  1fv  10373  4fvwrd4  10374  fzo0ss1  10410  fzo01  10460  fzo12sn  10461  fzo0to2pr  10462  fzo0to3tp  10463  fzo0to42pr  10464  zsupssdc  10497  qbtwnxr  10516  flval  10531  fldiv4lem1div2  10566  modqfrac  10598  modqmulnn  10603  q2txmodxeq0  10645  frecuzrdgdom  10679  frecuzrdgfun  10681  frecuzrdgsuct  10685  frechashgf1o  10689  nnct  10696  xnn0nnen  10698  fxnn0nninf  10700  0tonninf  10701  1tonninf  10702  iseqvalcbv  10720  ser0f  10795  0exp0e1  10805  qexpcl  10816  qexpclz  10821  m1expcl2  10822  1exp  10829  sqvali  10880  sqcli  10881  sqeq0i  10882  resqcli  10885  sq1  10894  neg1sqe1  10895  iexpcyc  10905  qsqeqor  10911  facnn  10988  fac0  10989  fac1  10990  fac2  10992  fac3  10993  fac4  10994  bcval  11010  bcm1k  11021  bcpasc  11027  bccl  11028  4bc3eq4  11034  4bc2eq6  11035  hashinfom  11039  hashennn  11041  hashfz1  11044  fihasheq0  11054  hash0  11057  hashsng  11059  fihashen1  11060  en1hash  11061  omgadd  11064  hashp1i  11073  hashxp  11089  fimaxq  11090  zfz1iso  11104  hash2en  11106  wrdexi  11125  wrdv  11128  wrdeqi  11135  wrd0  11137  lsw0  11160  ccatclab  11170  ccatidid  11186  s1prc  11199  ccat1st1st  11217  swrds1  11248  fnpfx  11257  swrdccatin2  11309  pfxccatin12lem2  11311  cats1fvn  11344  shftidt2  11392  cjexp  11453  re0  11455  im0  11456  re1  11457  im1  11458  cj0  11461  cji  11462  recli  11471  imcli  11472  cjcli  11473  replimi  11474  cjcji  11475  reim0bi  11476  rerebi  11477  cjrebi  11478  recji  11479  imcji  11480  cjmulrcli  11481  cjmulvali  11482  cjmulge0i  11483  renegi  11484  imnegi  11485  cjnegi  11486  addcji  11487  uzin2  11547  rexanuz  11548  rexfiuz  11549  sqrtrval  11560  sqrt0  11564  resqrexlemcalc3  11576  resqrexlemcvg  11579  resqrex  11586  abs0  11618  absi  11619  qabsor  11635  absimle  11644  recan  11669  caubnd2  11677  leabsi  11688  absrei  11689  sqrtpclii  11690  sqrtgt0ii  11691  absvalsqi  11700  absvalsq2i  11701  abscli  11702  absge0i  11703  absval2i  11704  abs00i  11705  absgt0api  11706  absnegi  11707  abscji  11708  releabsi  11709  infxrnegsupex  11823  xrbdtri  11836  cbvsum  11920  sumeq1i  11923  sum0  11948  isumz  11949  fisumss  11952  fsumsersdc  11955  fsumadd  11966  isumclim  11981  isumclim3  11983  fsumcnv  11997  modfsummodlem1  12016  fsumrelem  12031  binomlem  12043  binom  12044  arisum2  12059  expcnv  12064  0.999...  12081  prodf1f  12103  cbvprod  12118  prodeq1i  12121  zproddc  12139  zprodap0  12141  prod0  12145  fprodssdc  12150  prodsnf  12152  fprodcnv  12185  fprodge0  12197  fprodge1  12199  ef0lem  12220  esum  12222  ere  12230  ege2le3  12231  ef0  12232  eff2  12240  efsep  12251  reeff1  12260  sin0  12289  cos0  12290  ef01bndlem  12316  cos2bnd  12320  sincos1sgn  12325  sincos2sgn  12326  sin4lt0  12327  eirr  12339  0dvds  12371  dvds1  12413  z0even  12471  n2dvdsm1  12473  z2even  12474  n2dvds3  12475  ndvdssub  12490  ndvdsi  12493  flodddiv4  12496  bits0  12508  bitsfzo  12515  0bits  12519  m1bits  12520  bitsinv1lem  12521  bitsinv1  12522  gcddvds  12533  gcd1  12557  6gcd4e2  12565  bezoutlembi  12575  dfgcd3  12580  dfgcd2  12584  nninfctlemfo  12610  nninfct  12611  3lcm2e6woprm  12657  qredeu  12668  isprm2lem  12687  isprm3  12689  prm2orodd  12697  isprm5lem  12712  sqrt2irr0  12735  pw2dvds  12737  phicl2  12785  phi1  12790  dfphi2  12791  phiprmpw  12793  eulerthlemrprm  12800  eulerthlemh  12802  odzval  12813  oddprm  12831  pczpre  12869  pcdiv  12874  pc0  12876  pcqdiv  12879  pcrec  12880  pcexp  12881  pcxcl  12883  pcxqcl  12884  pcdvdstr  12899  pc2dvds  12902  dvdsprmpweqnn  12908  pcmpt  12915  qexpz  12924  pockthi  12930  1arith2  12940  4sqlemffi  12968  4sqlem11  12973  4sqlem13m  12975  4sqlem19  12981  dec2dvds  12983  dec5nprm  12986  modxai  12988  modxp1i  12990  numexp0  12994  numexp1  12995  ennnfonelemp1  13026  ennnfonelem1  13027  ennnfonelemkh  13032  ennnfonelemex  13034  ennnfonelemnn0  13042  ennnfonelemr  13043  exmidunben  13046  ctinfomlemom  13047  ctinfom  13048  ctinf  13050  qnnen  13051  omctfn  13063  omiunct  13064  ssnnctlemct  13066  nninfdc  13073  structcnvcnv  13097  structfun  13099  structfn  13100  ndxarg  13104  ndxid  13105  setsresg  13119  setsslnid  13133  basmex  13141  basmexd  13142  strleun  13186  strle1g  13188  prdsex  13351  prdsvallem  13354  prdsval  13355  prdsbaslemss  13356  imasaddfnlemg  13396  quslem  13406  xpsfrnel  13426  xpsff1o  13431  ismgmn0  13440  fn0g  13457  0g0  13458  fngsum  13470  idghm  13845  rhmfn  14185  rmodislmodlem  14363  rmodislmod  14364  lidlmex  14488  mopnset  14565  cntopex  14567  cnfldex  14572  cnfldbas  14573  mpocnfldadd  14574  mpocnfldmul  14576  cnfldcj  14578  cnfldtset  14579  cnfldle  14580  cnfldds  14581  cnring  14583  cnfld0  14584  cnfld1  14585  cnfldneg  14586  cnfldplusf  14587  cnfldsub  14588  cnfldmulg  14589  cnfldexp  14590  cnsubglem  14592  cnsubrglem  14593  gzsubrg  14595  gsumfzfsumlem0  14599  cnfldui  14602  zringring  14606  zringabl  14607  zringgrp  14608  zring1  14614  zringsubgval  14618  expghmap  14620  znval  14649  znle  14650  znbaslemnn  14652  znbas  14657  znzrh2  14659  znzrhval  14660  znzrhfo  14661  znleval  14666  znidom  14670  znidomb  14671  fnpsr  14680  psrelbas  14688  psradd  14692  psraddcl  14693  psr1clfi  14701  mplrcl  14707  mplbasss  14709  mpladd  14717  istopon  14736  topontopi  14739  toponunii  14740  toponrestid  14744  istps  14755  topontopn  14760  eltpsi  14764  eltg4i  14778  eltg3  14780  tg1  14782  tg2  14783  tgclb  14788  topnex  14809  sn0topon  14811  distps  14814  cldrcl  14825  sn0cld  14860  restco  14897  lmrcl  14915  ssidcn  14933  cnconst2  14956  cnptopresti  14961  cnptoprest  14962  txuni2  14979  txbas  14981  eltx  14982  txcnp  14994  upxp  14995  txcnmpt  14996  uptx  14997  txcn  14998  txrest  14999  txlm  15002  cnmptid  15004  cnmpt1st  15011  cnmpt2nd  15012  hmeofn  15025  psmetge0  15054  ismeti  15069  xmetunirn  15081  xmetge0  15088  unirnblps  15145  unirnbl  15146  mopnex  15228  qtopbasss  15244  retop  15247  uniretop  15248  iooretopg  15251  cnxmet  15254  cntoptopon  15255  cnbl0  15257  cnfldxms  15260  cnfldtps  15261  rexmet  15272  blssioo  15276  tgioo  15277  tgqioo  15278  cnopnap  15334  hovercncf  15369  limcresi  15389  dvfvalap  15404  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvcnp2cntop  15422  dvcoapbr  15430  dvexp2  15435  dvrecap  15436  dveflem  15449  dvef  15450  plyun0  15459  plyrecj  15486  dvply2  15490  reeff1o  15496  sin0pilem1  15504  sin0pilem2  15505  pilem3  15506  pigt2lt4  15507  pire  15509  sinhalfpilem  15514  pidiv2halves  15518  cosneghalfpi  15521  cospi  15523  efipi  15524  sin2pi  15526  cos2pi  15527  ef2pi  15528  cosq14gt0  15555  coseq00topi  15558  coseq0negpitopi  15559  sincos4thpi  15563  sincos6thpi  15565  sincos3rdpi  15566  pigt3  15567  cos02pilt1  15574  ioocosf1o  15577  dfrelog  15583  relogf1o  15584  relogcl  15585  relogiso  15596  rpcxpsqrt  15645  rpabscxpbnd  15663  2logb9irr  15694  2logb9irrALT  15697  sqrt2cxp2logb9e3  15698  2irrexpq  15699  2logb9irrap  15700  2irrexpqap  15701  mpodvdsmulf1o  15713  fsumdvdsmul  15714  perfectlem2  15723  lgsdir2lem1  15756  lgsdir2lem2  15757  lgsdir2lem4  15759  lgsdir2lem5  15760  lgsdi  15765  gausslemma2dlem0i  15785  gausslemma2dlem4  15792  lgseisenlem4  15801  lgsquadlem1  15805  lgsquad2lem2  15810  lgsquad2  15811  m1lgs  15813  2lgs2  15830  2lgslem4  15831  2lgsoddprmlem2  15834  2lgsoddprmlem3c  15837  2lgsoddprmlem3d  15838  2sqlem9  15852  2sqlem10  15853  1vgrex  15870  vtxval0  15903  iedgval0  15904  uhgr0  15935  upgrfi  15952  umgrislfupgrdom  15981  ausgrusgrben  16018  uspgredgiedg  16028  uspgriedgedg  16029  usgrislfuspgrdom  16040  uspgredg2vlem  16070  uspgredg2v  16071  usgr0  16089  griedg0prc  16100  subupgr  16123  vdegp1cid  16166  0wlk0  16221  clwwlkn1  16268  clwwlkn2  16271  eupth2lem1  16308  ex-fl  16321  ex-ceil  16322  ex-exp  16323  ex-fac  16324  ex-gcd  16327  bj-stfal  16338  bj-stst  16341  bj-dcfal  16351  bj-dcdc  16355  bj-stdc  16356  bj-dcst  16357  bj-el2oss1o  16370  elabf2  16378  bd0  16419  bdeli  16441  bdcriota  16478  bdbm1.3ii  16486  bdinex1  16494  bdssexi  16498  bj-inex  16502  bj-snex  16508  bj-sucex  16518  bj-d0clsepcl  16520  bj-omind  16529  bj-om  16532  bj-2inf  16533  bj-peano2  16534  bdpeano5  16538  bj-omssonALT  16558  bj-inf2vnlem1  16565  bj-omex2  16572  bj-nn0sucALT  16573  3dom  16587  012of  16592  2o01f  16593  subctctexmid  16601  pw1dceq  16605  nninfall  16611  nninfsellemqall  16617  nninfsellemeqinf  16618  nninfomnilem  16620  nninfomni  16621  exmidsbthrlem  16626  sbthom  16630  isomninnlem  16634  isomninn  16635  cvgcmp2nlemabs  16636  iooreen  16639  trilpolemisumle  16642  trilpolemeq1  16644  trilpo  16647  trirec0  16648  apdifflemr  16651  iswomninnlem  16653  iswomninn  16654  ismkvnnlem  16656  ismkvnn  16657  redcwlpo  16659  dcapnconst  16665  nconstwlpolem0  16667  nconstwlpo  16670  neapmkv  16672  neap0mkv  16673  taupi  16677