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  707  ori  731  orci  739  olci  740  biorfi  754  imorri  757  dcbii  848  simp1i  1033  simp2i  1034  simp3i  1035  3mix1i  1196  3mix2i  1197  3mix3i  1198  3jaoi  1340  mptru  1407  dfnot  1416  mptnan  1468  mtpor  1470  mtpxor  1471  dcfromnotnotr  1493  dcfromcon  1494  dcfrompeirce  1495  mpg  1500  19.23h  1547  hbequid  1562  axi12  1563  nfri  1568  spi  1585  19.21  1632  eximii  1651  19.35i  1674  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  2368  neeq1i  2418  neeq2i  2419  necon3i  2451  rspec  2585  rgen2a  2587  mprg  2590  r19.21  2609  r19.23  2642  raleqi  2735  rexeqi  2736  rabeqif  2794  elv  2807  elexi  2816  ceqsal  2833  vtocl3  2861  vtoclef  2880  vtocle  2881  spcv  2901  spcev  2902  clel3  2942  elabf  2950  elab2  2955  elab3  2959  euxfrdc  2993  reueq  3006  rmoimi2  3010  sbsbc  3036  sbc8g  3040  sbc6  3058  sbcie  3067  sbcrex  3112  csbvarg  3156  csbief  3173  csbie2  3178  sbnfc2  3189  sseli  3224  sselii  3225  sseq1i  3254  sseq2i  3255  difeq1i  3323  difeq2i  3324  uneq1i  3359  uneq2i  3360  ineq1i  3406  ineq2i  3407  ssinss1  3438  difdif2ss  3466  n0ii  3505  ne0ii  3506  vn0  3507  vn0m  3508  abf  3540  disj2  3552  difid  3565  0dif  3568  disjdif  3569  difin0  3570  undif1ss  3571  difdifdirss  3581  iftruei  3615  iffalsei  3618  ifbieq2i  3633  ifbieq12i  3635  pweqi  3660  pwid  3671  sneqi  3685  elsn  3689  elpr  3694  elsn2  3707  ralsn  3716  rexsn  3717  eltp  3721  rabrsndc  3743  preq1i  3755  preq2i  3756  prid1  3781  snnz  3795  snm  3796  prnz  3799  prm  3800  tpnz  3802  snss  3813  snsssn  3849  opeq1i  3870  opeq2i  3871  unieqi  3908  unissi  3921  inteqi  3937  intmin2  3959  intab  3962  intsn  3968  iinconstm  3984  iuniin  3985  iinss1  3987  iunxdif2  4024  ssiinf  4025  iinss  4027  iinss2  4028  iinab  4037  iundif2ss  4041  iindif2m  4043  iinin2m  4044  iunxsn  4052  iunxprg  4056  iinpw  4066  invdisjrab  4087  sndisj  4089  disjxsn  4091  breqi  4099  breq1i  4100  breq2i  4101  brab1  4141  opabbii  4161  truni  4206  bm1.3ii  4215  a9evsep  4216  ax9vsep  4217  zfnuleu  4218  axnul  4219  ssexi  4232  rabex  4239  rabex2  4241  elpw2  4252  pwnss  4255  iin0r  4265  intv  4266  pwex  4279  snex  4281  notnotsnex  4283  ord3ex  4286  dtruarb  4287  undifexmid  4289  intid  4322  opnzi  4333  copsexg  4342  opwo0id  4347  opelopabf  4375  epelc  4394  elon  4477  inton  4496  onn0  4503  onm  4504  elsuc  4509  elsuc2  4510  sucid  4520  iunsuc  4523  onordi  4529  ontrci  4530  onelssi  4532  eusvnf  4556  ssonunii  4593  sucex  4603  onssi  4619  onsuci  4620  ordtriexmidlem  4623  ordtriexmidlem2  4624  ordtriexmid  4625  ontriexmidim  4626  ordtri2orexmid  4627  2ordpr  4628  ontr2exmid  4629  onsucsssucexmid  4631  onsucelsucexmid  4634  regexmidlemm  4636  reg2exmid  4640  onirri  4647  ruALT  4655  onprc  4656  sucon  4657  dtru  4664  0elsucexmid  4669  ordpwsucexmid  4674  ordtri2or2exmid  4675  ontri2orexmidim  4676  dcextest  4685  omex  4697  find  4703  omelon  4713  nnoni  4715  limom  4718  nnregexmid  4725  omsinds  4726  xpeq1i  4751  xpeq2i  4752  0nelxp  4759  opthprc  4783  mosubop  4798  releqi  4815  relssi  4823  relin1  4851  relin2  4852  reldif  4853  inopab  4868  difopab  4869  xpiindim  4873  opabbi2dv  4885  ideq  4888  coeq1i  4895  coeq2i  4896  cnveqi  4911  eldm  4934  eldm2  4935  dmeqi  4938  dmv  4953  rneqi  4966  elrnmpti  4991  dmex  5005  rnex  5006  reseq1i  5015  reseq2i  5016  residm  5051  resex  5060  resmpt3  5068  imaeq1i  5079  imaeq2i  5080  elima  5087  imaex  5097  elimasn  5110  args  5112  epini  5114  dfse2  5116  eliniseg2  5123  relbrcnv  5124  cotr  5125  issref  5126  cnvsym  5127  asymref  5129  intirr  5130  codir  5132  qfto  5133  ssrnres  5186  cnveq0  5200  cnvsn0  5212  dmsnop  5217  rnsnop  5224  resdm2  5234  dfco2a  5244  cocnvcnv1  5254  coi2  5260  coires1  5261  cnvssrndm  5265  cossxp  5266  cocnvres  5268  relrelss  5270  relcoi2  5274  unidmrn  5276  dfdm2  5278  unixpm  5279  cnvexg  5281  cnvex  5282  cnviinm  5285  iotaval  5305  funeqi  5354  funi  5365  funres  5374  funcnvsn  5382  funcnvcnv  5396  funin  5408  funcnvres  5410  isarep2  5424  fneq1i  5431  fneq2i  5432  fndmi  5437  fnresdisj  5449  fnresi  5457  mpt0  5467  dmmpti  5469  feq1i  5482  feq2i  5483  fdmi  5497  fun2  5517  fssres  5520  resasplitss  5524  fintm  5530  fconst6  5545  f1ores  5607  foimacnv  5610  resdif  5614  funcocnv2  5617  f10d  5628  f1ovi  5633  fveq1i  5649  fveq2i  5651  0fv  5686  fvun1  5721  fvopab3ig  5729  fvmptss2  5730  mptrcl  5738  elfvmptrab1  5750  fndmdif  5761  fneqeql2  5765  f1oresrab  5820  fmptco  5821  funopsn  5838  fnressn  5848  fressnfv  5849  fmptap  5852  fvsnun1  5859  fvsnun2  5860  fsnunfv  5863  fconst2  5879  mptex  5890  fnfvimad  5900  riotabiia  6000  acexmidlema  6019  acexmidlemb  6020  acexmidlemcase  6023  acexmidlem2  6025  acexmidlemv  6026  oveq1i  6038  oveq2i  6039  oveqi  6041  oprabidlem  6059  0neqopab  6076  oprabbii  6086  oprabss  6117  mpompt  6123  funoprab  6131  fnoprab  6134  ovigg  6152  elmpocl  6227  relmptopab  6234  resfunexgALT  6279  cofunexg  6280  mptexw  6284  opabex3d  6292  opabex3  6293  1st0  6316  2nd0  6317  op1st  6318  op2nd  6319  f1stres  6331  f2ndres  6332  fo1stresm  6333  fo2ndresm  6334  1stcof  6335  2ndcof  6336  1stexg  6339  2ndexg  6340  releldm2  6357  reldm  6358  dfoprab3  6363  mpomptsx  6371  mpompts  6372  fnmpoi  6377  dmmpo  6378  mpoexxg  6384  mpoexw  6387  1stconst  6395  2ndconst  6396  dfmpo  6397  algrflem  6403  algrflemg  6404  cnvoprab  6408  f1od2  6409  elmpom  6412  mpoxopn0yelv  6448  mpoxopoveq  6449  tposssxp  6458  brtpos2  6460  reldmtpos  6462  dftpos2  6470  dftpos4  6472  tpostpos  6473  tpostpos2  6474  tposfo  6480  tposf  6481  tposeqi  6486  tposex  6487  tposoprab  6489  issmo  6497  smores  6501  smores2  6503  iordsmo  6506  smo0  6507  tfrlem8  6527  tfrexlem  6543  tfr1onlem3  6547  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlemres  6558  tfri1dALT  6560  tfri2  6575  rdgisuc1  6593  rdg0  6596  frecfun  6604  frec0g  6606  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecrdg  6617  2on0  6635  xp01disj  6644  2oconcl  6650  fnoa  6658  oaexg  6659  fnom  6661  omexg  6662  fnoei  6663  oeiexg  6664  oei0  6670  oacl  6671  oasuc  6675  o1p1e2  6679  omsuc  6683  nna0r  6689  nnm0r  6690  1onn  6731  2onn  6732  3onn  6733  4onn  6734  2ssom  6735  eqerlem  6776  eceq2i  6783  elqs  6798  qsex  6804  ecqs  6809  iinerm  6819  th3qlem1  6849  th3q  6852  mapsn  6902  mapsnf1o3  6909  ixpiinm  6936  ixpssmap  6944  brdom  6964  f1dom  6976  enref  6981  dom2  6991  idssen  6993  ssdomg  6995  ensymi  6999  ensn1  7013  fiprc  7033  1domsn  7044  dom1o  7045  xpcomf1o  7052  xpcomco  7053  dom0  7067  0dom  7068  xpmapenlem  7078  phplem2  7082  php5  7087  snnen2og  7088  1nen2  7090  php5dom  7092  ssfilem  7105  ssfiexmid  7106  ssfilemd  7107  ssfiexmidt  7108  domfiexmid  7110  0fi  7116  diffitest  7119  findcard  7120  findcard2  7121  findcard2s  7122  isinfinf  7129  ac6sfi  7130  inffiexmid  7141  pw1fin  7145  unfiexmid  7153  xpfi  7167  fisseneq  7170  ssfirab  7172  residfi  7182  en1eqsn  7190  snexxph  7192  sbthlem2  7200  sbthlemi3  7201  sbthlemi6  7204  sbthlem7  7205  fi0  7234  supeq1i  7247  infeq1i  7272  djuexb  7303  djuf1olemr  7313  inresflem  7319  djuinr  7322  updjudhcoinlf  7339  updjudhcoinrg  7340  casefun  7344  caserel  7346  caseinj  7348  caseinl  7350  caseinr  7351  omp1eomlem  7353  endjusym  7355  difinfsn  7359  difinfinf  7360  djuinj  7365  0ct  7366  ctmlemr  7367  ctssdclemn0  7369  ctssdccl  7370  omct  7376  ctfoex  7377  finomni  7399  exmidomni  7401  fodjuomni  7408  ctssexmid  7409  fodjumkv  7419  nninfwlporlem  7432  nninfwlpoimlemg  7434  nninfwlpoim  7438  nninfinfwlpo  7439  card0  7452  ficardon  7453  exmidonfinlem  7464  dju1p1e2  7468  exmidfodomrlemim  7472  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  iftrueb01  7501  3nelsucpw1  7512  sucpw1nss3  7513  3nsssucpw1  7514  fmelpw1o  7525  2onetap  7534  exmidmotap  7540  0npi  7593  dmaddpi  7605  dmmulpi  7606  1lt2pi  7620  0nnq  7644  1nq  7646  dmaddpq  7659  dmmulpq  7660  rec1nq  7675  1lt2nq  7686  halfnqq  7690  prarloclemarch2  7699  enq0enq  7711  nqnq0pi  7718  nnnq0lem1  7726  addnnnq0  7729  mulnnnq0  7730  nq0m0r  7736  addpinq1  7744  prarloclem5  7780  prarloclemcalc  7782  1pr  7834  1idprl  7870  1idpru  7871  ltexprlemm  7880  recexprlem1ssl  7913  recexprlem1ssu  7914  suplocexprlemell  7993  suplocexprlem2b  7994  suplocexprlemmu  7998  suplocexprlemdisj  8000  suplocexprlemloc  8001  suplocexprlemub  8003  suplocexprlemlub  8004  prsrlem1  8022  addsrpr  8025  mulsrpr  8026  gt0srpr  8028  0nsr  8029  0r  8030  1sr  8031  m1r  8032  m1m1sr  8041  caucvgsr  8082  suplocsrlempr  8087  addresr  8117  mulresr  8118  pitonnlem1  8125  peano1nnnn  8132  axi2m1  8155  axcnre  8161  peano5nnnn  8172  axcaucvg  8180  mpomulf  8229  mulridi  8241  mullidi  8242  pnfnre  8280  mnfnre  8281  pnfnemnf  8293  mnfxr  8295  rexri  8296  ltnri  8331  ltleii  8341  00id  8379  addridi  8380  addlidi  8381  0cnALT  8428  negeqi  8432  negicn  8439  neg0  8484  renegcli  8500  negcli  8506  negidi  8507  negnegi  8508  subidi  8509  subid1i  8510  negne0bi  8511  negrebi  8512  mul02i  8628  mul01i  8629  mulm1i  8641  leidi  8724  gt0ne0ii  8726  inelr  8823  msqge0i  8856  gt0ap0ii  8867  1div1e1  8943  div1i  8979  eqnegi  8980  recclapi  8981  recidapi  8982  divmulapi  9005  rerecclapi  9016  redivclapi  9018  rerecapb  9082  recgt0  9089  ltp1i  9144  divgt0ii  9158  ltmul1ii  9167  ltdiv1ii  9168  sup3exmid  9196  peano5nni  9205  nnrei  9211  1nn  9213  nngt0i  9232  neg1ap0  9311  2timesi  9332  times2i  9333  2nn  9364  3nn  9365  4nn  9366  5nn  9367  6nn  9368  7nn  9369  8nn  9370  9nn  9371  2muline0  9428  rehalfcli  9452  nn0ssre  9465  nnnn0i  9469  dfn2  9474  0nn0  9476  nn0ge0i  9488  zrei  9546  neg1z  9572  nn0negzi  9575  dfz2  9613  nneoi  9645  peano5uzi  9650  dfuzi  9651  nn0ind-raph  9658  deceq1i  9678  deceq2i  9679  10nn  9687  numltc  9697  eluzel2  9821  eluz1i  9824  nn0uz  9852  nnuz  9853  uzuzle35  9860  infrenegsupex  9889  lbzbi  9911  divfnzn  9916  qdivcl  9938  irrmul  9942  irrmulap  9943  cnref1o  9946  0ltpnf  10078  mnflt0  10080  0lepnf  10086  xrltnsym  10089  xrlttri3  10093  nltpnft  10110  ngtmnft  10113  xrrebnd  10115  xnegmnf  10125  xneg0  10127  xltnegi  10131  xaddmnf1  10144  xaddmnf2  10145  mnfaddpnf  10147  xaddid1  10158  xnn0lenn0nn0  10161  xnn0xadd0  10163  xposdif  10178  ixxex  10195  iooval2  10211  unirnioo  10269  ioorebasg  10271  elrege0  10272  fzval2  10308  fzen  10340  fzprval  10379  fztpval  10380  uzdisj  10390  ige2m1fz  10407  fz01or  10408  fz1ssfz0  10414  fz0sn  10418  fz0tp  10419  fz0to3un2pr  10420  fz0to4untppr  10421  nn0disj  10435  1fv  10436  4fvwrd4  10437  fzo0ss1  10473  fzo01  10524  fzo12sn  10525  fzo0to2pr  10526  fzo0to3tp  10527  fzo0to42pr  10528  zsupssdc  10561  qbtwnxr  10580  flval  10595  fldiv4lem1div2  10630  modqfrac  10662  modqmulnn  10667  q2txmodxeq0  10709  frecuzrdgdom  10743  frecuzrdgfun  10745  frecuzrdgsuct  10749  frechashgf1o  10753  nnct  10760  xnn0nnen  10762  fxnn0nninf  10764  0tonninf  10765  1tonninf  10766  iseqvalcbv  10784  ser0f  10859  0exp0e1  10869  qexpcl  10880  qexpclz  10885  m1expcl2  10886  1exp  10893  sqvali  10944  sqcli  10945  sqeq0i  10946  resqcli  10949  sq1  10958  neg1sqe1  10959  iexpcyc  10969  qsqeqor  10975  facnn  11052  fac0  11053  fac1  11054  fac2  11056  fac3  11057  fac4  11058  bcval  11074  bcm1k  11085  bcpasc  11091  bccl  11092  4bc3eq4  11098  4bc2eq6  11099  hashinfom  11103  hashennn  11105  hashfz1  11108  fihasheq0  11118  hash0  11121  hashsng  11123  fihashen1  11124  en1hash  11125  omgadd  11128  hashp1i  11137  hashxp  11153  fimaxq  11154  zfz1iso  11168  hash2en  11170  wrdexi  11192  wrdv  11195  wrdeqi  11202  wrd0  11204  lsw0  11227  ccatclab  11237  ccatidid  11253  s1prc  11266  ccat1st1st  11284  swrds1  11315  fnpfx  11324  swrdccatin2  11376  pfxccatin12lem2  11378  cats1fvn  11411  shftidt2  11472  cjexp  11533  re0  11535  im0  11536  re1  11537  im1  11538  cj0  11541  cji  11542  recli  11551  imcli  11552  cjcli  11553  replimi  11554  cjcji  11555  reim0bi  11556  rerebi  11557  cjrebi  11558  recji  11559  imcji  11560  cjmulrcli  11561  cjmulvali  11562  cjmulge0i  11563  renegi  11564  imnegi  11565  cjnegi  11566  addcji  11567  uzin2  11627  rexanuz  11628  rexfiuz  11629  sqrtrval  11640  sqrt0  11644  resqrexlemcalc3  11656  resqrexlemcvg  11659  resqrex  11666  abs0  11698  absi  11699  qabsor  11715  absimle  11724  recan  11749  caubnd2  11757  leabsi  11768  absrei  11769  sqrtpclii  11770  sqrtgt0ii  11771  absvalsqi  11780  absvalsq2i  11781  abscli  11782  absge0i  11783  absval2i  11784  abs00i  11785  absgt0api  11786  absnegi  11787  abscji  11788  releabsi  11789  infxrnegsupex  11903  xrbdtri  11916  cbvsum  12000  sumeq1i  12003  sum0  12029  isumz  12030  fisumss  12033  fsumsersdc  12036  fsumadd  12047  isumclim  12062  isumclim3  12064  fsumcnv  12078  modfsummodlem1  12097  fsumrelem  12112  binomlem  12124  binom  12125  arisum2  12140  expcnv  12145  0.999...  12162  prodf1f  12184  cbvprod  12199  prodeq1i  12202  zproddc  12220  zprodap0  12222  prod0  12226  fprodssdc  12231  prodsnf  12233  fprodcnv  12266  fprodge0  12278  fprodge1  12280  ef0lem  12301  esum  12303  ere  12311  ege2le3  12312  ef0  12313  eff2  12321  efsep  12332  reeff1  12341  sin0  12370  cos0  12371  ef01bndlem  12397  cos2bnd  12401  sincos1sgn  12406  sincos2sgn  12407  sin4lt0  12408  eirr  12420  0dvds  12452  dvds1  12494  z0even  12552  n2dvdsm1  12554  z2even  12555  n2dvds3  12556  ndvdssub  12571  ndvdsi  12574  flodddiv4  12577  bits0  12589  bitsfzo  12596  0bits  12600  m1bits  12601  bitsinv1lem  12602  bitsinv1  12603  gcddvds  12614  gcd1  12638  6gcd4e2  12646  bezoutlembi  12656  dfgcd3  12661  dfgcd2  12665  nninfctlemfo  12691  nninfct  12692  3lcm2e6woprm  12738  qredeu  12749  isprm2lem  12768  isprm3  12770  prm2orodd  12778  isprm5lem  12793  sqrt2irr0  12816  pw2dvds  12818  phicl2  12866  phi1  12871  dfphi2  12872  phiprmpw  12874  eulerthlemrprm  12881  eulerthlemh  12883  odzval  12894  oddprm  12912  pczpre  12950  pcdiv  12955  pc0  12957  pcqdiv  12960  pcrec  12961  pcexp  12962  pcxcl  12964  pcxqcl  12965  pcdvdstr  12980  pc2dvds  12983  dvdsprmpweqnn  12989  pcmpt  12996  qexpz  13005  pockthi  13011  1arith2  13021  4sqlemffi  13049  4sqlem11  13054  4sqlem13m  13056  4sqlem19  13062  dec2dvds  13064  dec5nprm  13067  modxai  13069  modxp1i  13071  numexp0  13075  numexp1  13076  ennnfonelemp1  13107  ennnfonelem1  13108  ennnfonelemkh  13113  ennnfonelemex  13115  ennnfonelemnn0  13123  ennnfonelemr  13124  exmidunben  13127  ctinfomlemom  13128  ctinfom  13129  ctinf  13131  qnnen  13132  omctfn  13144  omiunct  13145  ssnnctlemct  13147  nninfdc  13154  structcnvcnv  13178  structfun  13180  structfn  13181  ndxarg  13185  ndxid  13186  setsresg  13200  setsslnid  13214  basmex  13222  basmexd  13223  strleun  13267  strle1g  13269  prdsex  13432  prdsvallem  13435  prdsval  13436  prdsbaslemss  13437  imasaddfnlemg  13477  quslem  13487  xpsfrnel  13507  xpsff1o  13512  ismgmn0  13521  fn0g  13538  0g0  13539  fngsum  13551  idghm  13926  rhmfn  14267  rmodislmodlem  14446  rmodislmod  14447  lidlmex  14571  mopnset  14648  cntopex  14650  cnfldex  14655  cnfldbas  14656  mpocnfldadd  14657  mpocnfldmul  14659  cnfldcj  14661  cnfldtset  14662  cnfldle  14663  cnfldds  14664  cnring  14666  cnfld0  14667  cnfld1  14668  cnfldneg  14669  cnfldplusf  14670  cnfldsub  14671  cnfldmulg  14672  cnfldexp  14673  cnsubglem  14675  cnsubrglem  14676  gzsubrg  14678  gsumfzfsumlem0  14682  cnfldui  14685  zringring  14689  zringabl  14690  zringgrp  14691  zring1  14697  zringsubgval  14701  expghmap  14703  znval  14732  znle  14733  znbaslemnn  14735  znbas  14740  znzrh2  14742  znzrhval  14743  znzrhfo  14744  znleval  14749  znidom  14753  znidomb  14754  fnpsr  14763  psrelbas  14776  psradd  14780  psraddcl  14781  psr1clfi  14789  mplrcl  14795  mplbasss  14797  mpladd  14805  istopon  14824  topontopi  14827  toponunii  14828  toponrestid  14832  istps  14843  topontopn  14848  eltpsi  14852  eltg4i  14866  eltg3  14868  tg1  14870  tg2  14871  tgclb  14876  topnex  14897  sn0topon  14899  distps  14902  cldrcl  14913  sn0cld  14948  restco  14985  lmrcl  15003  ssidcn  15021  cnconst2  15044  cnptopresti  15049  cnptoprest  15050  txuni2  15067  txbas  15069  eltx  15070  txcnp  15082  upxp  15083  txcnmpt  15084  uptx  15085  txcn  15086  txrest  15087  txlm  15090  cnmptid  15092  cnmpt1st  15099  cnmpt2nd  15100  hmeofn  15113  psmetge0  15142  ismeti  15157  xmetunirn  15169  xmetge0  15176  unirnblps  15233  unirnbl  15234  mopnex  15316  qtopbasss  15332  retop  15335  uniretop  15336  iooretopg  15339  cnxmet  15342  cntoptopon  15343  cnbl0  15345  cnfldxms  15348  cnfldtps  15349  rexmet  15360  blssioo  15364  tgioo  15365  tgqioo  15366  cnopnap  15422  hovercncf  15457  limcresi  15477  dvfvalap  15492  dvidlemap  15502  dvidrelem  15503  dvidsslem  15504  dvcnp2cntop  15510  dvcoapbr  15518  dvexp2  15523  dvrecap  15524  dveflem  15537  dvef  15538  plyun0  15547  plyrecj  15574  dvply2  15578  reeff1o  15584  sin0pilem1  15592  sin0pilem2  15593  pilem3  15594  pigt2lt4  15595  pire  15597  sinhalfpilem  15602  pidiv2halves  15606  cosneghalfpi  15609  cospi  15611  efipi  15612  sin2pi  15614  cos2pi  15615  ef2pi  15616  cosq14gt0  15643  coseq00topi  15646  coseq0negpitopi  15647  sincos4thpi  15651  sincos6thpi  15653  sincos3rdpi  15654  pigt3  15655  cos02pilt1  15662  ioocosf1o  15665  dfrelog  15671  relogf1o  15672  relogcl  15673  relogiso  15684  rpcxpsqrt  15733  rpabscxpbnd  15751  2logb9irr  15782  2logb9irrALT  15785  sqrt2cxp2logb9e3  15786  2irrexpq  15787  2logb9irrap  15788  2irrexpqap  15789  mpodvdsmulf1o  15804  fsumdvdsmul  15805  perfectlem2  15814  lgsdir2lem1  15847  lgsdir2lem2  15848  lgsdir2lem4  15850  lgsdir2lem5  15851  lgsdi  15856  gausslemma2dlem0i  15876  gausslemma2dlem4  15883  lgseisenlem4  15892  lgsquadlem1  15896  lgsquad2lem2  15901  lgsquad2  15902  m1lgs  15904  2lgs2  15921  2lgslem4  15922  2lgsoddprmlem2  15925  2lgsoddprmlem3c  15928  2lgsoddprmlem3d  15929  2sqlem9  15943  2sqlem10  15944  1vgrex  15961  vtxval0  15994  iedgval0  15995  uhgr0  16026  upgrfi  16043  umgrislfupgrdom  16072  ausgrusgrben  16109  uspgredgiedg  16119  uspgriedgedg  16120  usgrislfuspgrdom  16131  uspgredg2vlem  16161  uspgredg2v  16162  usgr0  16180  griedg0prc  16191  subupgr  16214  vdegp1cid  16257  0wlk0  16312  clwwlkn1  16359  clwwlkn2  16362  eupth2lem1  16399  eulerpathum  16422  konigsbergiedgwen  16425  konigsberglem1  16429  konigsberglem3  16431  konigsberglem4  16432  konigsberglem5  16433  konigsberg  16434  ex-fl  16439  ex-ceil  16440  ex-exp  16441  ex-fac  16442  ex-gcd  16445  bj-stfal  16460  bj-stst  16463  bj-dcfal  16473  bj-dcdc  16477  bj-stdc  16478  bj-dcst  16479  bj-el2oss1o  16492  elabf2  16500  bd0  16540  bdeli  16562  bdcriota  16599  bdbm1.3ii  16607  bdinex1  16615  bdssexi  16619  bj-inex  16623  bj-snex  16629  bj-sucex  16639  bj-d0clsepcl  16641  bj-omind  16650  bj-om  16653  bj-2inf  16654  bj-peano2  16655  bdpeano5  16659  bj-omssonALT  16679  bj-inf2vnlem1  16686  bj-omex2  16693  bj-nn0sucALT  16694  3dom  16708  012of  16713  2o01f  16714  subctctexmid  16722  pw1dceq  16726  exmidpeirce  16729  nninfall  16735  nninfsellemqall  16741  nninfsellemeqinf  16742  nninfomnilem  16744  nninfomni  16745  exmidsbthrlem  16750  sbthom  16754  isomninnlem  16762  isomninn  16763  cvgcmp2nlemabs  16764  iooreen  16767  trilpolemisumle  16770  trilpolemeq1  16772  trilpo  16775  trirec0  16776  apdifflemr  16779  qdiff  16781  iswomninnlem  16782  iswomninn  16783  ismkvnnlem  16785  ismkvnn  16786  redcwlpo  16788  dcapnconst  16794  nconstwlpolem0  16796  nconstwlpo  16799  neapmkv  16801  neap0mkv  16802  taupi  16806  gfsumsn  16814  gfsumcl  16816