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  5830  fnressn  5840  fressnfv  5841  fmptap  5844  fvsnun1  5851  fvsnun2  5852  fsnunfv  5855  fconst2  5871  mptex  5880  fnfvimad  5890  riotabiia  5990  acexmidlema  6009  acexmidlemb  6010  acexmidlemcase  6013  acexmidlem2  6015  acexmidlemv  6016  oveq1i  6028  oveq2i  6029  oveqi  6031  oprabidlem  6049  0neqopab  6066  oprabbii  6076  oprabss  6107  mpompt  6113  funoprab  6121  fnoprab  6124  ovigg  6142  elmpocl  6217  relmptopab  6224  resfunexgALT  6270  cofunexg  6271  mptexw  6275  opabex3d  6283  opabex3  6284  1st0  6307  2nd0  6308  op1st  6309  op2nd  6310  f1stres  6322  f2ndres  6323  fo1stresm  6324  fo2ndresm  6325  1stcof  6326  2ndcof  6327  1stexg  6330  2ndexg  6331  releldm2  6348  reldm  6349  dfoprab3  6354  mpomptsx  6362  mpompts  6363  fnmpoi  6368  dmmpo  6369  mpoexxg  6375  mpoexw  6378  1stconst  6386  2ndconst  6387  dfmpo  6388  algrflem  6394  algrflemg  6395  cnvoprab  6399  f1od2  6400  elmpom  6403  mpoxopn0yelv  6405  mpoxopoveq  6406  tposssxp  6415  brtpos2  6417  reldmtpos  6419  dftpos2  6427  dftpos4  6429  tpostpos  6430  tpostpos2  6431  tposfo  6437  tposf  6438  tposeqi  6443  tposex  6444  tposoprab  6446  issmo  6454  smores  6458  smores2  6460  iordsmo  6463  smo0  6464  tfrlem8  6484  tfrexlem  6500  tfr1onlem3  6504  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlemres  6515  tfri1dALT  6517  tfri2  6532  rdgisuc1  6550  rdg0  6553  frecfun  6561  frec0g  6563  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecrdg  6574  2on0  6592  xp01disj  6601  2oconcl  6607  fnoa  6615  oaexg  6616  fnom  6618  omexg  6619  fnoei  6620  oeiexg  6621  oei0  6627  oacl  6628  oasuc  6632  o1p1e2  6636  omsuc  6640  nna0r  6646  nnm0r  6647  1onn  6688  2onn  6689  3onn  6690  4onn  6691  2ssom  6692  eqerlem  6733  eceq2i  6740  elqs  6755  qsex  6761  ecqs  6766  iinerm  6776  th3qlem1  6806  th3q  6809  mapsn  6859  mapsnf1o3  6866  ixpiinm  6893  ixpssmap  6901  brdom  6921  f1dom  6933  enref  6938  dom2  6948  idssen  6950  ssdomg  6952  ensymi  6956  ensn1  6970  fiprc  6990  1domsn  7001  dom1o  7002  xpcomf1o  7009  xpcomco  7010  dom0  7024  0dom  7025  xpmapenlem  7035  phplem2  7039  php5  7044  snnen2og  7045  1nen2  7047  php5dom  7049  ssfilem  7062  ssfiexmid  7063  ssfilemd  7064  ssfiexmidt  7065  domfiexmid  7067  0fi  7073  diffitest  7076  findcard  7077  findcard2  7078  findcard2s  7079  isinfinf  7086  ac6sfi  7087  inffiexmid  7098  pw1fin  7102  unfiexmid  7110  xpfi  7124  fisseneq  7127  ssfirab  7129  residfi  7139  en1eqsn  7147  snexxph  7149  sbthlem2  7157  sbthlemi3  7158  sbthlemi6  7161  sbthlem7  7162  fi0  7174  supeq1i  7187  infeq1i  7212  djuexb  7243  djuf1olemr  7253  inresflem  7259  djuinr  7262  updjudhcoinlf  7279  updjudhcoinrg  7280  casefun  7284  caserel  7286  caseinj  7288  caseinl  7290  caseinr  7291  omp1eomlem  7293  endjusym  7295  difinfsn  7299  difinfinf  7300  djuinj  7305  0ct  7306  ctmlemr  7307  ctssdclemn0  7309  ctssdccl  7310  omct  7316  ctfoex  7317  finomni  7339  exmidomni  7341  fodjuomni  7348  ctssexmid  7349  fodjumkv  7359  nninfwlporlem  7372  nninfwlpoimlemg  7374  nninfwlpoim  7378  nninfinfwlpo  7379  card0  7392  ficardon  7393  exmidonfinlem  7404  dju1p1e2  7408  exmidfodomrlemim  7412  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  iftrueb01  7441  3nelsucpw1  7452  sucpw1nss3  7453  3nsssucpw1  7454  2onetap  7474  exmidmotap  7480  0npi  7533  dmaddpi  7545  dmmulpi  7546  1lt2pi  7560  0nnq  7584  1nq  7586  dmaddpq  7599  dmmulpq  7600  rec1nq  7615  1lt2nq  7626  halfnqq  7630  prarloclemarch2  7639  enq0enq  7651  nqnq0pi  7658  nnnq0lem1  7666  addnnnq0  7669  mulnnnq0  7670  nq0m0r  7676  addpinq1  7684  prarloclem5  7720  prarloclemcalc  7722  1pr  7774  1idprl  7810  1idpru  7811  ltexprlemm  7820  recexprlem1ssl  7853  recexprlem1ssu  7854  suplocexprlemell  7933  suplocexprlem2b  7934  suplocexprlemmu  7938  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  suplocexprlemlub  7944  prsrlem1  7962  addsrpr  7965  mulsrpr  7966  gt0srpr  7968  0nsr  7969  0r  7970  1sr  7971  m1r  7972  m1m1sr  7981  caucvgsr  8022  suplocsrlempr  8027  addresr  8057  mulresr  8058  pitonnlem1  8065  peano1nnnn  8072  axi2m1  8095  axcnre  8101  peano5nnnn  8112  axcaucvg  8120  mpomulf  8169  mulridi  8181  mullidi  8182  pnfnre  8221  mnfnre  8222  pnfnemnf  8234  mnfxr  8236  rexri  8237  ltnri  8272  ltleii  8282  00id  8320  addridi  8321  addlidi  8322  0cnALT  8369  negeqi  8373  negicn  8380  neg0  8425  renegcli  8441  negcli  8447  negidi  8448  negnegi  8449  subidi  8450  subid1i  8451  negne0bi  8452  negrebi  8453  mul02i  8569  mul01i  8570  mulm1i  8582  leidi  8665  gt0ne0ii  8667  inelr  8764  msqge0i  8797  gt0ap0ii  8808  1div1e1  8884  div1i  8920  eqnegi  8921  recclapi  8922  recidapi  8923  divmulapi  8946  rerecclapi  8957  redivclapi  8959  rerecapb  9023  recgt0  9030  ltp1i  9085  divgt0ii  9099  ltmul1ii  9108  ltdiv1ii  9109  sup3exmid  9137  peano5nni  9146  nnrei  9152  1nn  9154  nngt0i  9173  neg1ap0  9252  2timesi  9273  times2i  9274  2nn  9305  3nn  9306  4nn  9307  5nn  9308  6nn  9309  7nn  9310  8nn  9311  9nn  9312  2muline0  9369  rehalfcli  9393  nn0ssre  9406  nnnn0i  9410  dfn2  9415  0nn0  9417  nn0ge0i  9429  zrei  9485  neg1z  9511  nn0negzi  9514  dfz2  9552  nneoi  9584  peano5uzi  9589  dfuzi  9590  nn0ind-raph  9597  deceq1i  9617  deceq2i  9618  10nn  9626  numltc  9636  eluzel2  9760  eluz1i  9763  nn0uz  9791  nnuz  9792  uzuzle35  9799  infrenegsupex  9828  lbzbi  9850  divfnzn  9855  qdivcl  9877  irrmul  9881  irrmulap  9882  cnref1o  9885  0ltpnf  10017  mnflt0  10019  0lepnf  10025  xrltnsym  10028  xrlttri3  10032  nltpnft  10049  ngtmnft  10052  xrrebnd  10054  xnegmnf  10064  xneg0  10066  xltnegi  10070  xaddmnf1  10083  xaddmnf2  10084  mnfaddpnf  10086  xaddid1  10097  xnn0lenn0nn0  10100  xnn0xadd0  10102  xposdif  10117  ixxex  10134  iooval2  10150  unirnioo  10208  ioorebasg  10210  elrege0  10211  fzval2  10246  fzen  10278  fzprval  10317  fztpval  10318  uzdisj  10328  ige2m1fz  10345  fz01or  10346  fz1ssfz0  10352  fz0sn  10356  fz0tp  10357  fz0to3un2pr  10358  fz0to4untppr  10359  nn0disj  10373  1fv  10374  4fvwrd4  10375  fzo0ss1  10411  fzo01  10462  fzo12sn  10463  fzo0to2pr  10464  fzo0to3tp  10465  fzo0to42pr  10466  zsupssdc  10499  qbtwnxr  10518  flval  10533  fldiv4lem1div2  10568  modqfrac  10600  modqmulnn  10605  q2txmodxeq0  10647  frecuzrdgdom  10681  frecuzrdgfun  10683  frecuzrdgsuct  10687  frechashgf1o  10691  nnct  10698  xnn0nnen  10700  fxnn0nninf  10702  0tonninf  10703  1tonninf  10704  iseqvalcbv  10722  ser0f  10797  0exp0e1  10807  qexpcl  10818  qexpclz  10823  m1expcl2  10824  1exp  10831  sqvali  10882  sqcli  10883  sqeq0i  10884  resqcli  10887  sq1  10896  neg1sqe1  10897  iexpcyc  10907  qsqeqor  10913  facnn  10990  fac0  10991  fac1  10992  fac2  10994  fac3  10995  fac4  10996  bcval  11012  bcm1k  11023  bcpasc  11029  bccl  11030  4bc3eq4  11036  4bc2eq6  11037  hashinfom  11041  hashennn  11043  hashfz1  11046  fihasheq0  11056  hash0  11059  hashsng  11061  fihashen1  11062  en1hash  11063  omgadd  11066  hashp1i  11075  hashxp  11091  fimaxq  11092  zfz1iso  11106  hash2en  11108  wrdexi  11130  wrdv  11133  wrdeqi  11140  wrd0  11142  lsw0  11165  ccatclab  11175  ccatidid  11191  s1prc  11204  ccat1st1st  11222  swrds1  11253  fnpfx  11262  swrdccatin2  11314  pfxccatin12lem2  11316  cats1fvn  11349  shftidt2  11410  cjexp  11471  re0  11473  im0  11474  re1  11475  im1  11476  cj0  11479  cji  11480  recli  11489  imcli  11490  cjcli  11491  replimi  11492  cjcji  11493  reim0bi  11494  rerebi  11495  cjrebi  11496  recji  11497  imcji  11498  cjmulrcli  11499  cjmulvali  11500  cjmulge0i  11501  renegi  11502  imnegi  11503  cjnegi  11504  addcji  11505  uzin2  11565  rexanuz  11566  rexfiuz  11567  sqrtrval  11578  sqrt0  11582  resqrexlemcalc3  11594  resqrexlemcvg  11597  resqrex  11604  abs0  11636  absi  11637  qabsor  11653  absimle  11662  recan  11687  caubnd2  11695  leabsi  11706  absrei  11707  sqrtpclii  11708  sqrtgt0ii  11709  absvalsqi  11718  absvalsq2i  11719  abscli  11720  absge0i  11721  absval2i  11722  abs00i  11723  absgt0api  11724  absnegi  11725  abscji  11726  releabsi  11727  infxrnegsupex  11841  xrbdtri  11854  cbvsum  11938  sumeq1i  11941  sum0  11967  isumz  11968  fisumss  11971  fsumsersdc  11974  fsumadd  11985  isumclim  12000  isumclim3  12002  fsumcnv  12016  modfsummodlem1  12035  fsumrelem  12050  binomlem  12062  binom  12063  arisum2  12078  expcnv  12083  0.999...  12100  prodf1f  12122  cbvprod  12137  prodeq1i  12140  zproddc  12158  zprodap0  12160  prod0  12164  fprodssdc  12169  prodsnf  12171  fprodcnv  12204  fprodge0  12216  fprodge1  12218  ef0lem  12239  esum  12241  ere  12249  ege2le3  12250  ef0  12251  eff2  12259  efsep  12270  reeff1  12279  sin0  12308  cos0  12309  ef01bndlem  12335  cos2bnd  12339  sincos1sgn  12344  sincos2sgn  12345  sin4lt0  12346  eirr  12358  0dvds  12390  dvds1  12432  z0even  12490  n2dvdsm1  12492  z2even  12493  n2dvds3  12494  ndvdssub  12509  ndvdsi  12512  flodddiv4  12515  bits0  12527  bitsfzo  12534  0bits  12538  m1bits  12539  bitsinv1lem  12540  bitsinv1  12541  gcddvds  12552  gcd1  12576  6gcd4e2  12584  bezoutlembi  12594  dfgcd3  12599  dfgcd2  12603  nninfctlemfo  12629  nninfct  12630  3lcm2e6woprm  12676  qredeu  12687  isprm2lem  12706  isprm3  12708  prm2orodd  12716  isprm5lem  12731  sqrt2irr0  12754  pw2dvds  12756  phicl2  12804  phi1  12809  dfphi2  12810  phiprmpw  12812  eulerthlemrprm  12819  eulerthlemh  12821  odzval  12832  oddprm  12850  pczpre  12888  pcdiv  12893  pc0  12895  pcqdiv  12898  pcrec  12899  pcexp  12900  pcxcl  12902  pcxqcl  12903  pcdvdstr  12918  pc2dvds  12921  dvdsprmpweqnn  12927  pcmpt  12934  qexpz  12943  pockthi  12949  1arith2  12959  4sqlemffi  12987  4sqlem11  12992  4sqlem13m  12994  4sqlem19  13000  dec2dvds  13002  dec5nprm  13005  modxai  13007  modxp1i  13009  numexp0  13013  numexp1  13014  ennnfonelemp1  13045  ennnfonelem1  13046  ennnfonelemkh  13051  ennnfonelemex  13053  ennnfonelemnn0  13061  ennnfonelemr  13062  exmidunben  13065  ctinfomlemom  13066  ctinfom  13067  ctinf  13069  qnnen  13070  omctfn  13082  omiunct  13083  ssnnctlemct  13085  nninfdc  13092  structcnvcnv  13116  structfun  13118  structfn  13119  ndxarg  13123  ndxid  13124  setsresg  13138  setsslnid  13152  basmex  13160  basmexd  13161  strleun  13205  strle1g  13207  prdsex  13370  prdsvallem  13373  prdsval  13374  prdsbaslemss  13375  imasaddfnlemg  13415  quslem  13425  xpsfrnel  13445  xpsff1o  13450  ismgmn0  13459  fn0g  13476  0g0  13477  fngsum  13489  idghm  13864  rhmfn  14205  rmodislmodlem  14383  rmodislmod  14384  lidlmex  14508  mopnset  14585  cntopex  14587  cnfldex  14592  cnfldbas  14593  mpocnfldadd  14594  mpocnfldmul  14596  cnfldcj  14598  cnfldtset  14599  cnfldle  14600  cnfldds  14601  cnring  14603  cnfld0  14604  cnfld1  14605  cnfldneg  14606  cnfldplusf  14607  cnfldsub  14608  cnfldmulg  14609  cnfldexp  14610  cnsubglem  14612  cnsubrglem  14613  gzsubrg  14615  gsumfzfsumlem0  14619  cnfldui  14622  zringring  14626  zringabl  14627  zringgrp  14628  zring1  14634  zringsubgval  14638  expghmap  14640  znval  14669  znle  14670  znbaslemnn  14672  znbas  14677  znzrh2  14679  znzrhval  14680  znzrhfo  14681  znleval  14686  znidom  14690  znidomb  14691  fnpsr  14700  psrelbas  14708  psradd  14712  psraddcl  14713  psr1clfi  14721  mplrcl  14727  mplbasss  14729  mpladd  14737  istopon  14756  topontopi  14759  toponunii  14760  toponrestid  14764  istps  14775  topontopn  14780  eltpsi  14784  eltg4i  14798  eltg3  14800  tg1  14802  tg2  14803  tgclb  14808  topnex  14829  sn0topon  14831  distps  14834  cldrcl  14845  sn0cld  14880  restco  14917  lmrcl  14935  ssidcn  14953  cnconst2  14976  cnptopresti  14981  cnptoprest  14982  txuni2  14999  txbas  15001  eltx  15002  txcnp  15014  upxp  15015  txcnmpt  15016  uptx  15017  txcn  15018  txrest  15019  txlm  15022  cnmptid  15024  cnmpt1st  15031  cnmpt2nd  15032  hmeofn  15045  psmetge0  15074  ismeti  15089  xmetunirn  15101  xmetge0  15108  unirnblps  15165  unirnbl  15166  mopnex  15248  qtopbasss  15264  retop  15267  uniretop  15268  iooretopg  15271  cnxmet  15274  cntoptopon  15275  cnbl0  15277  cnfldxms  15280  cnfldtps  15281  rexmet  15292  blssioo  15296  tgioo  15297  tgqioo  15298  cnopnap  15354  hovercncf  15389  limcresi  15409  dvfvalap  15424  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvcnp2cntop  15442  dvcoapbr  15450  dvexp2  15455  dvrecap  15456  dveflem  15469  dvef  15470  plyun0  15479  plyrecj  15506  dvply2  15510  reeff1o  15516  sin0pilem1  15524  sin0pilem2  15525  pilem3  15526  pigt2lt4  15527  pire  15529  sinhalfpilem  15534  pidiv2halves  15538  cosneghalfpi  15541  cospi  15543  efipi  15544  sin2pi  15546  cos2pi  15547  ef2pi  15548  cosq14gt0  15575  coseq00topi  15578  coseq0negpitopi  15579  sincos4thpi  15583  sincos6thpi  15585  sincos3rdpi  15586  pigt3  15587  cos02pilt1  15594  ioocosf1o  15597  dfrelog  15603  relogf1o  15604  relogcl  15605  relogiso  15616  rpcxpsqrt  15665  rpabscxpbnd  15683  2logb9irr  15714  2logb9irrALT  15717  sqrt2cxp2logb9e3  15718  2irrexpq  15719  2logb9irrap  15720  2irrexpqap  15721  mpodvdsmulf1o  15733  fsumdvdsmul  15734  perfectlem2  15743  lgsdir2lem1  15776  lgsdir2lem2  15777  lgsdir2lem4  15779  lgsdir2lem5  15780  lgsdi  15785  gausslemma2dlem0i  15805  gausslemma2dlem4  15812  lgseisenlem4  15821  lgsquadlem1  15825  lgsquad2lem2  15830  lgsquad2  15831  m1lgs  15833  2lgs2  15850  2lgslem4  15851  2lgsoddprmlem2  15854  2lgsoddprmlem3c  15857  2lgsoddprmlem3d  15858  2sqlem9  15872  2sqlem10  15873  1vgrex  15890  vtxval0  15923  iedgval0  15924  uhgr0  15955  upgrfi  15972  umgrislfupgrdom  16001  ausgrusgrben  16038  uspgredgiedg  16048  uspgriedgedg  16049  usgrislfuspgrdom  16060  uspgredg2vlem  16090  uspgredg2v  16091  usgr0  16109  griedg0prc  16120  subupgr  16143  vdegp1cid  16186  0wlk0  16241  clwwlkn1  16288  clwwlkn2  16291  eupth2lem1  16328  eulerpathum  16351  konigsbergiedgwen  16354  konigsberglem1  16358  konigsberglem3  16360  konigsberglem4  16361  konigsberglem5  16362  konigsberg  16363  ex-fl  16368  ex-ceil  16369  ex-exp  16370  ex-fac  16371  ex-gcd  16374  bj-stfal  16389  bj-stst  16392  bj-dcfal  16402  bj-dcdc  16406  bj-stdc  16407  bj-dcst  16408  bj-el2oss1o  16421  elabf2  16429  bd0  16470  bdeli  16492  bdcriota  16529  bdbm1.3ii  16537  bdinex1  16545  bdssexi  16549  bj-inex  16553  bj-snex  16559  bj-sucex  16569  bj-d0clsepcl  16571  bj-omind  16580  bj-om  16583  bj-2inf  16584  bj-peano2  16585  bdpeano5  16589  bj-omssonALT  16609  bj-inf2vnlem1  16616  bj-omex2  16623  bj-nn0sucALT  16624  3dom  16638  012of  16643  2o01f  16644  subctctexmid  16652  pw1dceq  16656  nninfall  16662  nninfsellemqall  16668  nninfsellemeqinf  16669  nninfomnilem  16671  nninfomni  16672  exmidsbthrlem  16677  sbthom  16681  isomninnlem  16685  isomninn  16686  cvgcmp2nlemabs  16687  iooreen  16690  trilpolemisumle  16693  trilpolemeq1  16695  trilpo  16698  trirec0  16699  apdifflemr  16702  qdiff  16704  iswomninnlem  16705  iswomninn  16706  ismkvnnlem  16708  ismkvnn  16709  redcwlpo  16711  dcapnconst  16717  nconstwlpolem0  16719  nconstwlpo  16722  neapmkv  16724  neap0mkv  16725  taupi  16729  gfsumsn  16737  gfsumcl  16739