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 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	⊢ 𝜑
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  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  3785  snm  3786  prnz  3789  prm  3790  tpnz  3792  snss  3802  snsssn  3838  opeq1i  3859  opeq2i  3860  unieqi  3897  unissi  3910  inteqi  3926  intmin2  3948  intab  3951  intsn  3957  iinconstm  3973  iuniin  3974  iinss1  3976  iunxdif2  4013  ssiinf  4014  iinss  4016  iinss2  4017  iinab  4026  iundif2ss  4030  iindif2m  4032  iinin2m  4033  iunxsn  4041  iunxprg  4045  iinpw  4055  invdisjrab  4076  sndisj  4078  disjxsn  4080  breqi  4088  breq1i  4089  breq2i  4090  brab1  4130  opabbii  4150  truni  4195  bm1.3ii  4204  a9evsep  4205  ax9vsep  4206  zfnuleu  4207  axnul  4208  ssexi  4221  rabex  4227  rabex2  4229  elpw2  4240  pwnss  4242  iin0r  4252  intv  4253  pwex  4266  snex  4268  notnotsnex  4270  ord3ex  4273  dtruarb  4274  undifexmid  4276  intid  4309  opnzi  4320  copsexg  4329  opwo0id  4334  opelopabf  4362  epelc  4381  elon  4464  inton  4483  onn0  4490  onm  4491  elsuc  4496  elsuc2  4497  sucid  4507  iunsuc  4510  onordi  4516  ontrci  4517  onelssi  4519  eusvnf  4543  ssonunii  4580  sucex  4590  onssi  4606  onsuci  4607  ordtriexmidlem  4610  ordtriexmidlem2  4611  ordtriexmid  4612  ontriexmidim  4613  ordtri2orexmid  4614  2ordpr  4615  ontr2exmid  4616  onsucsssucexmid  4618  onsucelsucexmid  4621  regexmidlemm  4623  reg2exmid  4627  onirri  4634  ruALT  4642  onprc  4643  sucon  4644  dtru  4651  0elsucexmid  4656  ordpwsucexmid  4661  ordtri2or2exmid  4662  ontri2orexmidim  4663  dcextest  4672  omex  4684  find  4690  omelon  4700  nnoni  4702  limom  4705  nnregexmid  4712  omsinds  4713  xpeq1i  4738  xpeq2i  4739  0nelxp  4746  opthprc  4769  mosubop  4784  releqi  4801  relssi  4809  relin1  4836  relin2  4837  reldif  4838  inopab  4853  difopab  4854  xpiindim  4858  opabbi2dv  4870  ideq  4873  coeq1i  4880  coeq2i  4881  cnveqi  4896  eldm  4919  eldm2  4920  dmeqi  4923  dmv  4938  rneqi  4951  elrnmpti  4976  dmex  4990  rnex  4991  reseq1i  5000  reseq2i  5001  residm  5036  resex  5045  resmpt3  5053  imaeq1i  5064  imaeq2i  5065  elima  5072  imaex  5082  elimasn  5094  args  5096  epini  5098  dfse2  5100  eliniseg2  5107  relbrcnv  5108  cotr  5109  issref  5110  cnvsym  5111  asymref  5113  intirr  5114  codir  5116  qfto  5117  ssrnres  5170  cnveq0  5184  cnvsn0  5196  dmsnop  5201  rnsnop  5208  resdm2  5218  dfco2a  5228  cocnvcnv1  5238  coi2  5244  coires1  5245  cnvssrndm  5249  cossxp  5250  cocnvres  5252  relrelss  5254  relcoi2  5258  unidmrn  5260  dfdm2  5262  unixpm  5263  cnvexg  5265  cnvex  5266  cnviinm  5269  iotaval  5289  funeqi  5338  funi  5349  funres  5358  funcnvsn  5365  funcnvcnv  5379  funin  5391  funcnvres  5393  isarep2  5407  fneq1i  5414  fneq2i  5415  fndmi  5420  fnresdisj  5432  fnresi  5440  mpt0  5450  dmmpti  5452  feq1i  5465  feq2i  5466  fdmi  5480  fun2  5497  fssres  5500  resasplitss  5504  fintm  5510  fconst6  5524  f1ores  5586  foimacnv  5589  resdif  5593  funcocnv2  5596  f10d  5606  f1ovi  5611  fveq1i  5627  fveq2i  5629  0fv  5664  fvun1  5699  fvopab3ig  5707  fvmptss2  5708  mptrcl  5716  elfvmptrab1  5728  fndmdif  5739  fneqeql2  5743  f1oresrab  5799  fmptco  5800  funopsn  5816  fnressn  5824  fressnfv  5825  fmptap  5828  fvsnun1  5835  fvsnun2  5836  fsnunfv  5839  fconst2  5855  mptex  5864  riotabiia  5972  acexmidlema  5991  acexmidlemb  5992  acexmidlemcase  5995  acexmidlem2  5997  acexmidlemv  5998  oveq1i  6010  oveq2i  6011  oveqi  6013  oprabidlem  6031  0neqopab  6048  oprabbii  6058  oprabss  6089  mpompt  6095  funoprab  6103  fnoprab  6106  ovigg  6124  elmpocl  6199  resfunexgALT  6251  cofunexg  6252  mptexw  6256  opabex3d  6264  opabex3  6265  1st0  6288  2nd0  6289  op1st  6290  op2nd  6291  f1stres  6303  f2ndres  6304  fo1stresm  6305  fo2ndresm  6306  1stcof  6307  2ndcof  6308  1stexg  6311  2ndexg  6312  releldm2  6329  reldm  6330  dfoprab3  6335  mpomptsx  6341  mpompts  6342  fnmpoi  6347  dmmpo  6348  mpoexxg  6354  mpoexw  6357  1stconst  6365  2ndconst  6366  dfmpo  6367  algrflem  6373  algrflemg  6374  cnvoprab  6378  f1od2  6379  mpoxopn0yelv  6383  mpoxopoveq  6384  tposssxp  6393  brtpos2  6395  reldmtpos  6397  dftpos2  6405  dftpos4  6407  tpostpos  6408  tpostpos2  6409  tposfo  6415  tposf  6416  tposeqi  6421  tposex  6422  tposoprab  6424  issmo  6432  smores  6436  smores2  6438  iordsmo  6441  smo0  6442  tfrlem8  6462  tfrexlem  6478  tfr1onlem3  6482  tfr1onlemsucaccv  6485  tfr1onlembxssdm  6487  tfr1onlemres  6493  tfri1dALT  6495  tfri2  6510  rdgisuc1  6528  rdg0  6531  frecfun  6539  frec0g  6541  freccllem  6546  frecfcllem  6548  frecsuclem  6550  frecrdg  6552  2on0  6570  xp01disj  6577  2oconcl  6583  fnoa  6591  oaexg  6592  fnom  6594  omexg  6595  fnoei  6596  oeiexg  6597  oei0  6603  oacl  6604  oasuc  6608  o1p1e2  6612  omsuc  6616  nna0r  6622  nnm0r  6623  1onn  6664  2onn  6665  3onn  6666  4onn  6667  2ssom  6668  eqerlem  6709  eceq2i  6716  elqs  6731  qsex  6737  ecqs  6742  iinerm  6752  th3qlem1  6782  th3q  6785  mapsn  6835  mapsnf1o3  6842  ixpiinm  6869  ixpssmap  6877  brdom  6897  f1dom  6909  enref  6914  dom2  6924  idssen  6926  ssdomg  6928  ensymi  6932  ensn1  6946  fiprc  6966  1domsn  6974  xpcomf1o  6980  xpcomco  6981  dom0  6995  0dom  6996  xpmapenlem  7006  phplem2  7010  php5  7015  snnen2og  7016  1nen2  7018  php5dom  7020  ssfilem  7033  ssfiexmid  7034  domfiexmid  7036  0fin  7042  diffitest  7045  findcard  7046  findcard2  7047  findcard2s  7048  isinfinf  7055  ac6sfi  7056  inffiexmid  7064  pw1fin  7068  unfiexmid  7076  xpfi  7090  fisseneq  7092  ssfirab  7094  residfi  7103  en1eqsn  7111  snexxph  7113  sbthlem2  7121  sbthlemi3  7122  sbthlemi6  7125  sbthlem7  7126  fi0  7138  supeq1i  7151  infeq1i  7176  djuexb  7207  djuf1olemr  7217  inresflem  7223  djuinr  7226  updjudhcoinlf  7243  updjudhcoinrg  7244  casefun  7248  caserel  7250  caseinj  7252  caseinl  7254  caseinr  7255  omp1eomlem  7257  endjusym  7259  difinfsn  7263  difinfinf  7264  djuinj  7269  0ct  7270  ctmlemr  7271  ctssdclemn0  7273  ctssdccl  7274  omct  7280  ctfoex  7281  finomni  7303  exmidomni  7305  fodjuomni  7312  ctssexmid  7313  fodjumkv  7323  nninfwlporlem  7336  nninfwlpoimlemg  7338  nninfwlpoim  7342  nninfinfwlpo  7343  card0  7356  ficardon  7357  exmidonfinlem  7367  dju1p1e2  7371  exmidfodomrlemim  7375  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  iftrueb01  7404  3nelsucpw1  7415  sucpw1nss3  7416  3nsssucpw1  7417  2onetap  7437  exmidmotap  7443  0npi  7496  dmaddpi  7508  dmmulpi  7509  1lt2pi  7523  0nnq  7547  1nq  7549  dmaddpq  7562  dmmulpq  7563  rec1nq  7578  1lt2nq  7589  halfnqq  7593  prarloclemarch2  7602  enq0enq  7614  nqnq0pi  7621  nnnq0lem1  7629  addnnnq0  7632  mulnnnq0  7633  nq0m0r  7639  addpinq1  7647  prarloclem5  7683  prarloclemcalc  7685  1pr  7737  1idprl  7773  1idpru  7774  ltexprlemm  7783  recexprlem1ssl  7816  recexprlem1ssu  7817  suplocexprlemell  7896  suplocexprlem2b  7897  suplocexprlemmu  7901  suplocexprlemdisj  7903  suplocexprlemloc  7904  suplocexprlemub  7906  suplocexprlemlub  7907  prsrlem1  7925  addsrpr  7928  mulsrpr  7929  gt0srpr  7931  0nsr  7932  0r  7933  1sr  7934  m1r  7935  m1m1sr  7944  caucvgsr  7985  suplocsrlempr  7990  addresr  8020  mulresr  8021  pitonnlem1  8028  peano1nnnn  8035  axi2m1  8058  axcnre  8064  peano5nnnn  8075  axcaucvg  8083  mpomulf  8132  mulridi  8144  mullidi  8145  pnfnre  8184  mnfnre  8185  pnfnemnf  8197  mnfxr  8199  rexri  8200  ltnri  8235  ltleii  8245  00id  8283  addridi  8284  addlidi  8285  0cnALT  8332  negeqi  8336  negicn  8343  neg0  8388  renegcli  8404  negcli  8410  negidi  8411  negnegi  8412  subidi  8413  subid1i  8414  negne0bi  8415  negrebi  8416  mul02i  8532  mul01i  8533  mulm1i  8545  leidi  8628  gt0ne0ii  8630  inelr  8727  msqge0i  8760  gt0ap0ii  8771  1div1e1  8847  div1i  8883  eqnegi  8884  recclapi  8885  recidapi  8886  divmulapi  8909  rerecclapi  8920  redivclapi  8922  rerecapb  8986  recgt0  8993  ltp1i  9048  divgt0ii  9062  ltmul1ii  9071  ltdiv1ii  9072  sup3exmid  9100  peano5nni  9109  nnrei  9115  1nn  9117  nngt0i  9136  neg1ap0  9215  2timesi  9236  times2i  9237  2nn  9268  3nn  9269  4nn  9270  5nn  9271  6nn  9272  7nn  9273  8nn  9274  9nn  9275  2muline0  9332  rehalfcli  9356  nn0ssre  9369  nnnn0i  9373  dfn2  9378  0nn0  9380  nn0ge0i  9392  zrei  9448  neg1z  9474  nn0negzi  9477  dfz2  9515  nneoi  9547  peano5uzi  9552  dfuzi  9553  nn0ind-raph  9560  deceq1i  9580  deceq2i  9581  10nn  9589  numltc  9599  eluzel2  9723  eluz1i  9725  nn0uz  9753  nnuz  9754  infrenegsupex  9785  lbzbi  9807  divfnzn  9812  qdivcl  9834  irrmul  9838  irrmulap  9839  cnref1o  9842  0ltpnf  9974  mnflt0  9976  0lepnf  9982  xrltnsym  9985  xrlttri3  9989  nltpnft  10006  ngtmnft  10009  xrrebnd  10011  xnegmnf  10021  xneg0  10023  xltnegi  10027  xaddmnf1  10040  xaddmnf2  10041  mnfaddpnf  10043  xaddid1  10054  xnn0lenn0nn0  10057  xnn0xadd0  10059  xposdif  10074  ixxex  10091  iooval2  10107  unirnioo  10165  ioorebasg  10167  elrege0  10168  fzval2  10203  fzen  10235  fzprval  10274  fztpval  10275  uzdisj  10285  ige2m1fz  10302  fz01or  10303  fz1ssfz0  10309  fz0sn  10313  fz0tp  10314  fz0to3un2pr  10315  fz0to4untppr  10316  nn0disj  10330  1fv  10331  4fvwrd4  10332  fzo0ss1  10368  fzo01  10417  fzo12sn  10418  fzo0to2pr  10419  fzo0to3tp  10420  fzo0to42pr  10421  zsupssdc  10453  qbtwnxr  10472  flval  10487  fldiv4lem1div2  10522  modqfrac  10554  modqmulnn  10559  q2txmodxeq0  10601  frecuzrdgdom  10635  frecuzrdgfun  10637  frecuzrdgsuct  10641  frechashgf1o  10645  nnct  10652  xnn0nnen  10654  fxnn0nninf  10656  0tonninf  10657  1tonninf  10658  iseqvalcbv  10676  ser0f  10751  0exp0e1  10761  qexpcl  10772  qexpclz  10777  m1expcl2  10778  1exp  10785  sqvali  10836  sqcli  10837  sqeq0i  10838  resqcli  10841  sq1  10850  neg1sqe1  10851  iexpcyc  10861  qsqeqor  10867  facnn  10944  fac0  10945  fac1  10946  fac2  10948  fac3  10949  fac4  10950  bcval  10966  bcm1k  10977  bcpasc  10983  bccl  10984  4bc3eq4  10990  4bc2eq6  10991  hashinfom  10995  hashennn  10997  hashfz1  11000  fihasheq0  11010  hash0  11013  hashsng  11015  fihashen1  11016  omgadd  11019  hashp1i  11027  hashxp  11043  fimaxq  11044  zfz1iso  11058  hash2en  11060  wrdexi  11079  wrdv  11082  wrdeqi  11089  wrd0  11091  lsw0  11114  ccatclab  11124  ccatidid  11140  s1prc  11151  ccat1st1st  11167  swrds1  11195  fnpfx  11204  swrdccatin2  11256  pfxccatin12lem2  11258  cats1fvn  11291  shftidt2  11338  cjexp  11399  re0  11401  im0  11402  re1  11403  im1  11404  cj0  11407  cji  11408  recli  11417  imcli  11418  cjcli  11419  replimi  11420  cjcji  11421  reim0bi  11422  rerebi  11423  cjrebi  11424  recji  11425  imcji  11426  cjmulrcli  11427  cjmulvali  11428  cjmulge0i  11429  renegi  11430  imnegi  11431  cjnegi  11432  addcji  11433  uzin2  11493  rexanuz  11494  rexfiuz  11495  sqrtrval  11506  sqrt0  11510  resqrexlemcalc3  11522  resqrexlemcvg  11525  resqrex  11532  abs0  11564  absi  11565  qabsor  11581  absimle  11590  recan  11615  caubnd2  11623  leabsi  11634  absrei  11635  sqrtpclii  11636  sqrtgt0ii  11637  absvalsqi  11646  absvalsq2i  11647  abscli  11648  absge0i  11649  absval2i  11650  abs00i  11651  absgt0api  11652  absnegi  11653  abscji  11654  releabsi  11655  infxrnegsupex  11769  xrbdtri  11782  cbvsum  11866  sumeq1i  11869  sum0  11894  isumz  11895  fisumss  11898  fsumsersdc  11901  fsumadd  11912  isumclim  11927  isumclim3  11929  fsumcnv  11943  modfsummodlem1  11962  fsumrelem  11977  binomlem  11989  binom  11990  arisum2  12005  expcnv  12010  0.999...  12027  prodf1f  12049  cbvprod  12064  prodeq1i  12067  zproddc  12085  zprodap0  12087  prod0  12091  fprodssdc  12096  prodsnf  12098  fprodcnv  12131  fprodge0  12143  fprodge1  12145  ef0lem  12166  esum  12168  ere  12176  ege2le3  12177  ef0  12178  eff2  12186  efsep  12197  reeff1  12206  sin0  12235  cos0  12236  ef01bndlem  12262  cos2bnd  12266  sincos1sgn  12271  sincos2sgn  12272  sin4lt0  12273  eirr  12285  0dvds  12317  dvds1  12359  z0even  12417  n2dvdsm1  12419  z2even  12420  n2dvds3  12421  ndvdssub  12436  ndvdsi  12439  flodddiv4  12442  bits0  12454  bitsfzo  12461  0bits  12465  m1bits  12466  bitsinv1lem  12467  bitsinv1  12468  gcddvds  12479  gcd1  12503  6gcd4e2  12511  bezoutlembi  12521  dfgcd3  12526  dfgcd2  12530  nninfctlemfo  12556  nninfct  12557  3lcm2e6woprm  12603  qredeu  12614  isprm2lem  12633  isprm3  12635  prm2orodd  12643  isprm5lem  12658  sqrt2irr0  12681  pw2dvds  12683  phicl2  12731  phi1  12736  dfphi2  12737  phiprmpw  12739  eulerthlemrprm  12746  eulerthlemh  12748  odzval  12759  oddprm  12777  pczpre  12815  pcdiv  12820  pc0  12822  pcqdiv  12825  pcrec  12826  pcexp  12827  pcxcl  12829  pcxqcl  12830  pcdvdstr  12845  pc2dvds  12848  dvdsprmpweqnn  12854  pcmpt  12861  qexpz  12870  pockthi  12876  1arith2  12886  4sqlemffi  12914  4sqlem11  12919  4sqlem13m  12921  4sqlem19  12927  dec2dvds  12929  dec5nprm  12932  modxai  12934  modxp1i  12936  numexp0  12940  numexp1  12941  ennnfonelemp1  12972  ennnfonelem1  12973  ennnfonelemkh  12978  ennnfonelemex  12980  ennnfonelemnn0  12988  ennnfonelemr  12989  exmidunben  12992  ctinfomlemom  12993  ctinfom  12994  ctinf  12996  qnnen  12997  omctfn  13009  omiunct  13010  ssnnctlemct  13012  nninfdc  13019  structcnvcnv  13043  structfun  13045  structfn  13046  ndxarg  13050  ndxid  13051  setsresg  13065  setsslnid  13079  basmex  13087  basmexd  13088  strleun  13132  strle1g  13134  prdsex  13297  prdsvallem  13300  prdsval  13301  prdsbaslemss  13302  imasaddfnlemg  13342  quslem  13352  xpsfrnel  13372  xpsff1o  13377  ismgmn0  13386  fn0g  13403  0g0  13404  fngsum  13416  idghm  13791  rhmfn  14130  rmodislmodlem  14308  rmodislmod  14309  lidlmex  14433  mopnset  14510  cntopex  14512  cnfldex  14517  cnfldbas  14518  mpocnfldadd  14519  mpocnfldmul  14521  cnfldcj  14523  cnfldtset  14524  cnfldle  14525  cnfldds  14526  cnring  14528  cnfld0  14529  cnfld1  14530  cnfldneg  14531  cnfldplusf  14532  cnfldsub  14533  cnfldmulg  14534  cnfldexp  14535  cnsubglem  14537  cnsubrglem  14538  gzsubrg  14540  gsumfzfsumlem0  14544  cnfldui  14547  zringring  14551  zringabl  14552  zringgrp  14553  zring1  14559  zringsubgval  14563  expghmap  14565  znval  14594  znle  14595  znbaslemnn  14597  znbas  14602  znzrh2  14604  znzrhval  14605  znzrhfo  14606  znleval  14611  znidom  14615  znidomb  14616  fnpsr  14625  psrelbas  14633  psradd  14637  psraddcl  14638  psr1clfi  14646  mplrcl  14652  mplbasss  14654  mpladd  14662  istopon  14681  topontopi  14684  toponunii  14685  toponrestid  14689  istps  14700  topontopn  14705  eltpsi  14709  eltg4i  14723  eltg3  14725  tg1  14727  tg2  14728  tgclb  14733  topnex  14754  sn0topon  14756  distps  14759  cldrcl  14770  sn0cld  14805  restco  14842  lmrcl  14859  ssidcn  14878  cnconst2  14901  cnptopresti  14906  cnptoprest  14907  txuni2  14924  txbas  14926  eltx  14927  txcnp  14939  upxp  14940  txcnmpt  14941  uptx  14942  txcn  14943  txrest  14944  txlm  14947  cnmptid  14949  cnmpt1st  14956  cnmpt2nd  14957  hmeofn  14970  psmetge0  14999  ismeti  15014  xmetunirn  15026  xmetge0  15033  unirnblps  15090  unirnbl  15091  mopnex  15173  qtopbasss  15189  retop  15192  uniretop  15193  iooretopg  15196  cnxmet  15199  cntoptopon  15200  cnbl0  15202  cnfldxms  15205  cnfldtps  15206  rexmet  15217  blssioo  15221  tgioo  15222  tgqioo  15223  cnopnap  15279  hovercncf  15314  limcresi  15334  dvfvalap  15349  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvcnp2cntop  15367  dvcoapbr  15375  dvexp2  15380  dvrecap  15381  dveflem  15394  dvef  15395  plyun0  15404  plyrecj  15431  dvply2  15435  reeff1o  15441  sin0pilem1  15449  sin0pilem2  15450  pilem3  15451  pigt2lt4  15452  pire  15454  sinhalfpilem  15459  pidiv2halves  15463  cosneghalfpi  15466  cospi  15468  efipi  15469  sin2pi  15471  cos2pi  15472  ef2pi  15473  cosq14gt0  15500  coseq00topi  15503  coseq0negpitopi  15504  sincos4thpi  15508  sincos6thpi  15510  sincos3rdpi  15511  pigt3  15512  cos02pilt1  15519  ioocosf1o  15522  dfrelog  15528  relogf1o  15529  relogcl  15530  relogiso  15541  rpcxpsqrt  15590  rpabscxpbnd  15608  2logb9irr  15639  2logb9irrALT  15642  sqrt2cxp2logb9e3  15643  2irrexpq  15644  2logb9irrap  15645  2irrexpqap  15646  mpodvdsmulf1o  15658  fsumdvdsmul  15659  perfectlem2  15668  lgsdir2lem1  15701  lgsdir2lem2  15702  lgsdir2lem4  15704  lgsdir2lem5  15705  lgsdi  15710  gausslemma2dlem0i  15730  gausslemma2dlem4  15737  lgseisenlem4  15746  lgsquadlem1  15750  lgsquad2lem2  15755  lgsquad2  15756  m1lgs  15758  2lgs2  15775  2lgslem4  15776  2lgsoddprmlem2  15779  2lgsoddprmlem3c  15782  2lgsoddprmlem3d  15783  2sqlem9  15797  2sqlem10  15798  1vgrex  15815  vtxval0  15848  iedgval0  15849  uhgr0  15879  upgrfi  15896  umgrislfupgrdom  15923  ausgrusgrben  15960  uspgredgiedg  15970  uspgriedgedg  15971  usgrislfuspgrdom  15982  uspgredg2vlem  16012  uspgredg2v  16013  ex-fl  16047  ex-ceil  16048  ex-exp  16049  ex-fac  16050  ex-gcd  16053  bj-stfal  16064  bj-stst  16067  bj-dcfal  16077  bj-dcdc  16081  bj-stdc  16082  bj-dcst  16083  bj-el2oss1o  16096  elabf2  16104  bd0  16145  bdeli  16167  bdcriota  16204  bdbm1.3ii  16212  bdinex1  16220  bdssexi  16224  bj-inex  16228  bj-snex  16234  bj-sucex  16244  bj-d0clsepcl  16246  bj-omind  16255  bj-om  16258  bj-2inf  16259  bj-peano2  16260  bdpeano5  16264  bj-omssonALT  16284  bj-inf2vnlem1  16291  bj-omex2  16298  bj-nn0sucALT  16299  dom1o  16314  012of  16316  2o01f  16317  subctctexmid  16325  nninfall  16334  nninfsellemqall  16340  nninfsellemeqinf  16341  nninfomnilem  16343  nninfomni  16344  exmidsbthrlem  16349  sbthom  16353  isomninnlem  16357  isomninn  16358  cvgcmp2nlemabs  16359  iooreen  16362  trilpolemisumle  16365  trilpolemeq1  16367  trilpo  16370  trirec0  16371  apdifflemr  16374  iswomninnlem  16376  iswomninn  16377  ismkvnnlem  16379  ismkvnn  16380  redcwlpo  16382  dcapnconst  16388  nconstwlpolem0  16390  nconstwlpo  16393  neapmkv  16395  neap0mkv  16396  taupi  16400