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

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 used 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  430  pm2.65i  648  notnoti  654  pm2.21i  655  pm2.24ii  656  notbii  678  nbn  711  ori  735  orci  743  olci  744  biorfi  758  imorri  761  dcbii  852  simp1i  1037  simp2i  1038  simp3i  1039  3mix1i  1200  3mix2i  1201  3mix3i  1202  3jaoi  1344  mptru  1411  dfnot  1420  mptnan  1472  mtpor  1474  mtpxor  1475  dcfromnotnotr  1497  dcfromcon  1498  dcfrompeirce  1499  mpg  1504  19.23h  1551  hbequid  1566  axi12  1567  nfri  1572  spi  1589  19.21  1636  eximii  1655  19.35i  1678  nfn  1710  19.37aiv  1727  19.23  1730  exan  1745  equid  1753  hbae  1770  equvini  1811  equveli  1812  sbid  1827  sbieh  1843  exdistrfor  1853  dveeq2or  1869  ax11v  1880  ax11ev  1881  equs5or  1883  sb4or  1886  sb4bor  1888  nfsb2or  1890  sbequilem  1891  sbequi  1892  speiv  1915  nfsbxy  2002  nfsbxyt  2003  sbco  2028  sbcocom  2030  sbcomxyyz  2032  sbal1yz  2061  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  eumoi  2119  moani  2157  elsb1  2216  elsb2  2217  eqeq1i  2246  eqeq2i  2249  eleq1i  2304  eleq2i  2305  nfcrii  2385  neeq1i  2435  neeq2i  2436  necon3i  2468  rspec  2602  rgen2a  2604  mprg  2607  r19.21  2626  r19.23  2659  raleqi  2753  rexeqi  2754  rabeqif  2812  elv  2825  elexi  2834  ceqsal  2851  vtocl3  2879  vtoclef  2898  vtocle  2899  spcv  2919  spcev  2920  clel3  2961  elabf  2969  elab2  2974  elab3  2978  euxfrdc  3012  reueq  3025  rmoimi2  3029  sbsbc  3055  sbc8g  3059  sbc6  3077  sbcie  3086  sbcrex  3131  csbvarg  3175  csbief  3192  csbie2  3197  sbnfc2  3208  sseli  3244  sselii  3245  sseq1i  3274  sseq2i  3275  difeq1i  3343  difeq2i  3344  uneq1i  3379  uneq2i  3380  ineq1i  3428  ineq2i  3429  ssinss1  3460  difdif2ss  3488  n0ii  3530  ne0ii  3531  vn0  3532  vn0m  3533  abf  3570  disj2  3580  difid  3594  0dif  3597  disjdif  3599  difin0  3601  undif1ss  3602  difdifdirss  3612  iftruei  3646  iffalsei  3649  ifbieq2i  3664  ifbieq12i  3666  pweqi  3692  sspwi  3703  pwid  3707  sneqi  3721  elsn  3725  elpr  3730  elsn2  3743  ralsn  3752  rexsn  3753  eltp  3757  rabrsndc  3779  preq1i  3791  preq2i  3792  prid1  3817  snnz  3832  snm  3833  prnz  3836  prm  3837  tpnz  3839  snss  3850  snsssn  3886  opeq1i  3907  opeq2i  3908  unieqi  3945  unissi  3958  inteqi  3974  intmin2  3996  intab  3999  intsn  4005  iinconstm  4021  iuniin  4022  iinss1  4024  iunxdif2  4061  ssiinf  4062  iinss  4064  iinss2  4065  iinab  4074  iundif2ss  4078  iindif2m  4080  iinin2m  4081  iunxsn  4089  iunxprg  4093  iinpw  4103  invdisjrab  4124  sndisj  4126  disjxsn  4129  breqi  4137  breq1i  4138  breq2i  4139  brab1  4179  opabbii  4199  truni  4245  sepgi  4254  bm1.3ii  4256  a9evsep  4257  ax9vsep  4258  zfnuleu  4259  axnul  4260  ssexi  4273  difexi  4278  rabex  4282  rabex2  4284  elpw2  4295  pwnss  4298  iin0r  4308  intv  4309  pwex  4322  snex  4324  notnotsnex  4326  ord3ex  4329  dtruarb  4330  undifexmid  4332  intid  4366  opnzi  4377  copsexg  4386  opwo0id  4391  opelopabf  4419  epelc  4438  elon  4521  inton  4540  onn0  4547  onm  4548  elsuc  4553  elsuc2  4554  sucid  4564  iunsuc  4567  onordi  4573  ontrci  4574  onelssi  4576  eusvnf  4601  ssonunii  4638  sucex  4648  onssi  4664  onsuci  4665  ordtriexmidlem  4668  ordtriexmidlem2  4669  ordtriexmid  4670  ontriexmidim  4671  ordtri2orexmid  4672  2ordpr  4673  ontr2exmid  4674  onsucsssucexmid  4676  onsucelsucexmid  4679  regexmidlemm  4681  reg2exmid  4685  onirri  4692  ruALT  4700  onprc  4701  sucon  4702  dtru  4709  0elsucexmid  4714  ordpwsucexmid  4719  ordtri2or2exmid  4720  ontri2orexmidim  4721  dcextest  4730  omex  4742  find  4748  omelon  4758  nnoni  4760  limom  4763  nnregexmid  4770  omsinds  4771  xpeq1i  4796  xpeq2i  4797  0nelxp  4804  opthprc  4828  mosubop  4843  releqi  4860  relssi  4868  relin1  4897  relin2  4898  reldif  4899  inopab  4914  difopab  4915  xpiindim  4919  opabbi2dv  4931  ideq  4934  coeq1i  4941  coeq2i  4942  cnveqi  4957  eldm  4980  eldm2  4981  dmeqi  4984  dmv  4999  rneqi  5012  elrnmpti  5037  dmex  5051  rnex  5052  reseq1i  5061  reseq2i  5062  residm  5097  resex  5107  resmpt3  5115  imaeq1i  5126  imaeq2i  5127  elima  5134  imaex  5144  elimasn  5157  args  5159  epini  5161  dfse2  5163  eliniseg2  5170  relbrcnv  5171  cotr  5172  issref  5173  cnvsym  5174  asymref  5176  intirr  5177  codir  5179  qfto  5180  ssrnres  5233  cnveq0  5247  cnvsn0  5259  dmsnop  5264  rnsnop  5271  resdm2  5281  dfco2a  5291  cocnvcnv1  5301  coi2  5307  coires1  5308  cnvssrndm  5312  cossxp  5313  cocnvres  5315  relrelss  5317  relcoi2  5321  unidmrn  5323  dfdm2  5325  unixpm  5326  cnvexg  5328  cnvex  5329  cnviinm  5332  iotaval  5352  funeqi  5401  funi  5412  funres  5421  funcnvsn  5429  funcnvcnv  5443  funin  5455  funcnvres  5457  isarep2  5471  fneq1i  5478  fneq2i  5479  fndmi  5484  fnresdisj  5496  fnresi  5504  mpt0  5514  dmmpti  5516  feq1i  5529  feq2i  5530  fdmi  5544  fun2  5565  fssres  5568  resasplitss  5572  fintm  5580  fconst6  5595  f1ores  5657  foimacnv  5660  resdif  5664  funcocnv2  5667  f10d  5678  f1ovi  5683  fveq1i  5699  fveq2i  5701  0fv  5737  fvun1  5772  fvopab3ig  5782  fvmptss2  5783  mptrcl  5791  elfvmptrab1  5804  fndmdif  5817  fneqeql2  5821  f1oresrab  5876  fmptco  5877  funopsn  5894  fnressn  5904  fressnfv  5905  fmptap  5908  fvsnun1  5915  fvsnun2  5916  fsnunfv  5919  fconst2  5935  mptex  5946  fnfvimad  5957  rinvf1o  6038  riotabiia  6060  acexmidlema  6079  acexmidlemb  6080  acexmidlemcase  6083  acexmidlem2  6085  acexmidlemv  6086  oveq1i  6098  oveq2i  6099  oveqi  6101  oprabidlem  6119  0neqopab  6136  oprabbii  6146  oprabss  6177  mpompt  6183  funoprab  6191  fnoprab  6194  ovigg  6212  elmpocl  6287  relmptopab  6294  resfunexgALT  6341  cofunexg  6342  mptexw  6346  opabex3d  6354  opabex3  6355  1st0  6382  2nd0  6383  op1st  6384  op2nd  6385  f1stres  6397  f2ndres  6398  fo1stresm  6399  fo2ndresm  6400  1stcof  6401  2ndcof  6402  1stexg  6405  2ndexg  6406  releldm2  6423  reldm  6424  dfoprab3  6429  mpomptsx  6437  mpompts  6438  fnmpoi  6443  dmmpo  6444  mpoexxg  6450  mpoexw  6453  1stconst  6461  2ndconst  6462  dfmpo  6463  algrflem  6469  algrflemg  6470  cnvoprab  6474  f1od2  6475  elmpom  6478  mpoxopn0yelv  6514  mpoxopoveq  6515  tposssxp  6524  brtpos2  6526  reldmtpos  6528  dftpos2  6536  dftpos4  6538  tpostpos  6539  tpostpos2  6540  tposfo  6546  tposf  6547  tposeqi  6552  tposex  6553  tposoprab  6555  issmo  6563  smores  6567  smores2  6569  iordsmo  6572  smo0  6573  tfrlem8  6593  tfrexlem  6609  tfr1onlem3  6613  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlemres  6624  tfri1dALT  6626  tfri2  6641  rdgisuc1  6659  rdg0  6662  frecfun  6670  frec0g  6672  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecrdg  6683  2on0  6701  xp01disj  6710  2oconcl  6716  fnoa  6724  oaexg  6725  fnom  6727  omexg  6728  fnoei  6729  oeiexg  6730  oei0  6736  oacl  6737  oasuc  6741  o1p1e2  6745  omsuc  6749  nna0r  6755  nnm0r  6756  1onn  6797  2onn  6798  3onn  6799  4onn  6800  2ssom  6801  eqerlem  6842  eceq2i  6849  elqs  6864  qsex  6870  ecqs  6875  iinerm  6885  th3qlem1  6915  th3q  6918  mapsn  6976  mapsnf1o3  6983  ixpiinm  7010  ixpssmap  7018  brdom  7038  f1dom  7050  enref  7055  dom2  7065  idssen  7067  ssdomg  7069  ensymi  7073  ensn1  7087  fiprc  7108  1domsn  7119  dom1o  7120  xpcomf1o  7127  xpcomco  7128  dom0  7142  0dom  7143  xpmapenlem  7153  phplem2  7158  php5  7163  snnen2og  7164  1nen2  7166  php5dom  7168  ssfilem  7181  ssfiexmid  7182  ssfilemd  7183  ssfiexmidt  7184  domfiexmid  7186  0fi  7192  diffitest  7195  findcard  7196  findcard2  7197  findcard2s  7198  isinfinf  7205  ac6sfi  7206  inffiexmid  7217  pw1fin  7221  unfiexmid  7229  xpfi  7243  fisseneq  7246  ssfirab  7248  residfi  7258  mapfi  7265  en1eqsn  7270  snexxph  7272  sbthlem2  7280  sbthlemi3  7281  sbthlemi6  7284  sbthlem7  7285  fi0  7314  fipwfi  7327  supeq1i  7334  infeq1i  7359  djuexb  7390  djuf1olemr  7400  inresflem  7406  djuinr  7409  updjudhcoinlf  7426  updjudhcoinrg  7427  casefun  7431  caserel  7433  caseinj  7435  caseinl  7437  caseinr  7438  omp1eomlem  7440  endjusym  7442  difinfsn  7446  difinfinf  7447  djuinj  7452  0ct  7453  ctmlemr  7454  ctssdclemn0  7456  ctssdccl  7457  omct  7463  ctfoex  7464  finomni  7486  exmidomni  7488  fodjuomni  7495  ctssexmid  7496  fodjumkv  7506  nninfwlporlem  7519  nninfwlpoimlemg  7521  nninfwlpoim  7525  nninfinfwlpo  7526  card0  7539  ficardon  7540  exmidonfinlem  7551  dju1p1e2  7555  exmidfodomrlemim  7559  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  iftrueb01  7588  3nelsucpw1  7599  sucpw1nss3  7600  3nsssucpw1  7601  fmelpw1o  7612  2onetap  7627  exmidmotap  7633  0npi  7686  dmaddpi  7698  dmmulpi  7699  1lt2pi  7713  0nnq  7737  1nq  7739  dmaddpq  7752  dmmulpq  7753  rec1nq  7768  1lt2nq  7779  halfnqq  7783  prarloclemarch2  7792  enq0enq  7804  nqnq0pi  7811  nnnq0lem1  7819  addnnnq0  7822  mulnnnq0  7823  nq0m0r  7829  addpinq1  7837  prarloclem5  7873  prarloclemcalc  7875  1pr  7927  1idprl  7963  1idpru  7964  ltexprlemm  7973  recexprlem1ssl  8006  recexprlem1ssu  8007  suplocexprlemell  8086  suplocexprlem2b  8087  suplocexprlemmu  8091  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemub  8096  suplocexprlemlub  8097  prsrlem1  8115  addsrpr  8118  mulsrpr  8119  gt0srpr  8121  0nsr  8122  0r  8123  1sr  8124  m1r  8125  m1m1sr  8134  caucvgsr  8175  suplocsrlempr  8180  addresr  8210  mulresr  8211  pitonnlem1  8218  peano1nnnn  8225  axi2m1  8248  axcnre  8254  peano5nnnn  8265  axcaucvg  8273  mpomulf  8322  mulridi  8334  mullidi  8335  pnfnre  8373  mnfnre  8374  pnfnemnf  8386  mnfxr  8388  rexri  8389  ltnri  8425  ltleii  8435  00id  8474  addridi  8475  addlidi  8476  0cnALT  8523  negeqi  8527  negicn  8534  neg0  8579  renegcli  8595  negcli  8601  negidi  8602  negnegi  8603  subidi  8604  subid1i  8605  negne0bi  8606  negrebi  8607  mul02i  8724  mul01i  8725  mulm1i  8737  leidi  8820  gt0ne0ii  8822  inelr  8920  msqge0i  8953  gt0ap0ii  8964  1div1e1  9042  div1i  9078  eqnegi  9079  recclapi  9080  recidapi  9081  divmulapi  9104  rerecclapi  9115  redivclapi  9117  rerecapb  9181  recgt0  9188  ltp1i  9243  divgt0ii  9257  ltmul1ii  9266  ltdiv1ii  9267  sup3exmid  9295  ofsubeq0  9300  indconst0  9311  indconst1  9312  peano5nni  9316  nnrei  9322  1nn  9324  nngt0i  9343  neg1ap0  9422  2timesi  9443  times2i  9444  2nn  9477  3nn  9478  4nn  9479  5nn  9480  6nn  9481  7nn  9482  8nn  9483  9nn  9484  2muline0  9541  rehalfcli  9565  nn0ssre  9578  nnnn0i  9582  dfn2  9587  0nn0  9589  nn0ge0i  9601  zrei  9661  neg1z  9687  nn0negzi  9690  dfz2  9728  nneoi  9761  peano5uzi  9766  dfuzi  9767  nn0ind-raph  9774  deceq1i  9794  deceq2i  9795  10nn  9807  numltc  9818  eluzel2  9942  eluz1i  9945  nn0uz  9973  nnuz  9974  uzuzle35  9981  infrenegsupex  10010  lbzbi  10032  divfnzn  10037  qdivcl  10059  irrmul  10064  irrmulap  10065  cnref1o  10068  0ltpnf  10201  mnflt0  10203  0lepnf  10209  xrltnsym  10212  xrlttri3  10216  nltpnft  10233  ngtmnft  10236  xrrebnd  10238  xnegmnf  10248  xneg0  10250  xltnegi  10254  xaddmnf1  10267  xaddmnf2  10268  mnfaddpnf  10270  xaddid1  10281  xnn0lenn0nn0  10284  xnn0xadd0  10286  xposdif  10301  ixxex  10318  iooval2  10334  unirnioo  10392  ioorebasg  10394  elrege0  10395  fzval2  10431  fzen  10464  fzprval  10506  fztpval  10507  uzdisj  10517  ige2m1fz  10534  fz01or  10535  fz1ssfz0  10541  fz0sn  10545  fz0tp  10546  fz0to3un2pr  10547  fz0to4untppr  10548  nn0disj  10562  1fv  10563  4fvwrd4  10564  fzo0ss1  10600  fzo01  10651  fzo12sn  10652  fzo0to2pr  10653  fzo0to3tp  10654  fzo0to42pr  10655  zsupssdc  10690  qbtwnxr  10709  flval  10724  flapcl  10728  flaplelt  10730  fldiv4lem1div2  10763  modqfrac  10795  modqmulnn  10800  q2txmodxeq0  10842  frecuzrdgdom  10876  frecuzrdgfun  10878  frecuzrdgsuct  10882  frechashgf1o  10886  nnct  10893  xnn0nnen  10895  fxnn0nninf  10897  0tonninf  10898  1tonninf  10899  iseqvalcbv  10917  ser0f  10992  0exp0e1  11002  qexpcl  11013  qexpclz  11018  m1expcl2  11019  1exp  11026  sqvali  11077  sqcli  11078  sqeq0i  11079  resqcli  11082  sq1  11091  neg1sqe1  11092  iexpcyc  11102  qsqeqor  11108  nn0sqdc  11168  facnn  11187  fac0  11188  fac1  11189  fac2  11191  fac3  11192  fac4  11193  bcval  11209  bcm1k  11220  bcpasc  11226  bccl  11227  4bc3eq4  11234  4bc2eq6  11235  hashinfom  11239  hashennn  11241  hashfz1  11244  fihasheq0  11254  hash0  11257  hashsng  11259  fihashen1  11260  en1hash  11261  omgadd  11264  hashp1i  11273  hashxp  11289  hashpwfi  11291  fimaxq  11292  ssenneg  11302  hashfibc  11305  hashf1lem1  11307  hashf1  11309  zfz1iso  11315  hash2en  11317  wrdexi  11339  wrdv  11342  wrdeqi  11349  wrd0  11351  lsw0  11374  ccatclab  11384  ccatidid  11400  s1prc  11413  ccat1st1st  11431  swrds1  11462  fnpfx  11471  swrdccatin2  11523  pfxccatin12lem2  11525  cats1fvn  11558  shftidt2  11619  cjexp  11680  re0  11683  im0  11684  re1  11685  im1  11686  cj0  11689  cji  11690  recli  11699  imcli  11700  cjcli  11701  replimi  11702  cjcji  11703  reim0bi  11704  rerebi  11705  cjrebi  11706  recji  11707  imcji  11708  cjmulrcli  11709  cjmulvali  11710  cjmulge0i  11711  renegi  11712  imnegi  11713  cjnegi  11714  addcji  11715  uzin2  11775  rexanuz  11776  rexfiuz  11777  sqrtrval  11788  sqrt0  11792  resqrexlemcalc3  11804  resqrexlemcvg  11807  resqrex  11814  abs0  11846  absi  11847  qabsor  11863  absimle  11873  recan  11898  caubnd2  11906  leabsi  11917  absrei  11918  sqrtpclii  11919  sqrtgt0ii  11920  absvalsqi  11929  absvalsq2i  11930  abscli  11931  absge0i  11932  absval2i  11933  abs00i  11934  absgt0api  11935  absnegi  11936  abscji  11937  releabsi  11938  infxrnegsupex  12054  xrbdtri  12067  cbvsum  12151  sumeq1i  12154  sum0  12180  isumz  12181  fisumss  12184  fsumsersdc  12187  fsumadd  12198  isumclim  12213  isumclim3  12215  fsumcnv  12229  modfsummodlem1  12248  fsumrelem  12263  binomlem  12275  binom  12276  arisum2  12291  expcnv  12296  0.999...  12313  prodf1f  12335  cbvprod  12350  prodeq1i  12353  zproddc  12371  zprodap0  12373  prod0  12377  fprodssdc  12382  prodsnf  12384  fprodcnv  12417  fprodge0  12429  fprodge1  12431  ef0lem  12452  esum  12454  ere  12462  ege2le3  12463  ef0  12464  eff2  12472  efsep  12483  reeff1  12492  sin0  12521  cos0  12522  ef01bndlem  12548  cos2bnd  12552  sincos1sgn  12557  sincos2sgn  12558  sin4lt0  12559  eirr  12571  0dvds  12603  dvds1  12645  z0even  12703  n2dvdsm1  12705  z2even  12706  n2dvds3  12707  ndvdssub  12722  ndvdsi  12725  flodddiv4  12728  bits0  12740  bitsfzo  12747  0bits  12751  m1bits  12752  bitsinv1lem  12753  bitsinv1  12754  gcddvds  12765  gcd1  12789  6gcd4e2  12797  bezoutlembi  12807  dfgcd3  12812  dfgcd2  12816  nninfctlemfo  12842  nninfct  12843  3lcm2e6woprm  12889  qredeu  12900  isprm2lem  12919  isprm3  12921  prm2orodd  12929  isprm5lem  12945  sqrt2irr0  12968  sqrtrirr  13014  phicl2  13021  phi1  13026  dfphi2  13027  phiprmpw  13029  eulerthlemrprm  13036  eulerthlemh  13038  odzval  13049  oddprm  13067  pczpre  13105  pcdiv  13110  pc0  13112  pcqdiv  13115  pcrec  13116  pcexp  13117  pcxcl  13119  pcxqcl  13120  pcdvdstr  13135  pc2dvds  13138  dvdsprmpweqnn  13144  pcmpt  13151  qexpz  13160  pockthi  13166  1arith2  13176  4sqlemffi  13204  4sqlem11  13209  4sqlem13m  13211  4sqlem19  13217  dec2dvds  13219  dec5nprm  13222  modxai  13224  modxp1i  13226  mod2xnegi  13227  numexp0  13231  numexp1  13232  1259lem5  13275  ballotfilem1  13278  ballotfilemonn  13279  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilem4  13299  ballotfilemi  13301  ballotfilem7  13337  ballotfilem8  13338  ballotfilemth  13339  ennnfonelemp1  13355  ennnfonelem1  13356  ennnfonelemkh  13361  ennnfonelemex  13363  ennnfonelemnn0  13371  ennnfonelemr  13372  exmidunben  13375  ctinfomlemom  13376  ctinfom  13377  ctinf  13379  qnnen  13380  omctfn  13392  omiunct  13393  ssnnctlemct  13395  nninfdc  13402  structcnvcnv  13426  structfun  13428  structfn  13429  ndxarg  13433  ndxid  13434  setsresg  13448  setsslnid  13462  basmex  13470  basmexd  13471  slotm  13473  strleun  13517  strle1g  13519  prdsvallem  13680  imasaddfnlemg  13694  quslem  13704  xpsfrnel  13724  xpsff1o  13729  ismgmn0  13737  fn0g  13754  0g0  13755  fngzsum  13767  idghm  14121  elcntr  14163  gsumsncmn  14246  gsumclfi  14249  gsummptfidmadd  14251  gsumsubmclfi  14253  gsummptfidmsplit  14254  gsumconstcmn  14266  gsum2dfilem2  14272  gsumcom2fi  14275  prdsex  14279  prdsval  14280  prdsbaslemss  14281  mgpplusg  14329  mgpbas  14332  ringidval  14372  rhmfn  14588  rmodislmodlem  14796  rmodislmod  14797  lidlmex  14921  mopnset  14998  cntopex  15000  cnfldex  15005  cnfldbas  15006  mpocnfldadd  15007  mpocnfldmul  15009  cnfldcj  15011  cnfldtset  15012  cnfldle  15013  cnfldds  15014  cnring  15016  cnfld0  15017  cnfld1  15018  cnfldneg  15019  cnfldplusf  15020  cnfldsub  15021  cnfldmulg  15022  cnfldexp  15023  cnsubglem  15025  cnsubrglem  15026  gzsubrg  15028  gsumfsum  15032  cnfldui  15033  zringring  15037  zringabl  15038  zringgrp  15039  zring1  15045  zringsubgval  15049  expghmap  15051  znval  15080  znle  15081  znbaslemnn  15083  znbas  15088  znzrh2  15090  znzrhval  15091  znzrhfo  15092  znleval  15097  znidom  15101  znidomb  15102  fnpsr  15160  psrass1filem  15177  psrelbas  15179  psradd  15183  psraddcl  15184  psrmulfval  15187  psr1clfi  15198  mplrcl  15210  mplbasss  15212  mpladd  15220  istopon  15239  topontopi  15242  toponunii  15243  toponrestid  15247  istps  15258  topontopn  15263  eltpsi  15267  eltg4i  15281  eltg3  15283  tg1  15285  tg2  15286  tgclb  15291  topnex  15312  sn0topon  15314  distps  15317  cldrcl  15328  sn0cld  15363  restco  15400  lmrcl  15418  ssidcn  15436  cnconst2  15459  cnptopresti  15464  cnptoprest  15465  txuni2  15482  txbas  15484  eltx  15485  txcnp  15497  upxp  15498  txcnmpt  15499  uptx  15500  txcn  15501  txrest  15502  txlm  15505  cnmptid  15507  cnmpt1st  15514  cnmpt2nd  15515  hmeofn  15528  psmetge0  15557  ismeti  15572  xmetunirn  15584  xmetge0  15591  unirnblps  15648  unirnbl  15649  mopnex  15731  qtopbasss  15747  retop  15750  uniretop  15751  iooretopg  15754  cnxmet  15757  cntoptopon  15758  cnbl0  15760  cnfldxms  15763  cnfldtps  15764  rexmet  15775  blssioo  15779  tgioo  15780  tgqioo  15781  cnopnap  15837  hovercncf  15872  limcresi  15892  dvfvalap  15907  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvcnp2cntop  15925  dvcoapbr  15933  dvexp2  15938  dvrecap  15939  dveflem  15952  dvef  15953  plyun0  15962  plyrecj  15989  dvply2  15993  reeff1o  15999  sin0pilem1  16008  sin0pilem2  16009  pilem3  16010  pigt2lt4  16011  pire  16013  sinhalfpilem  16018  pidiv2halves  16022  cosneghalfpi  16025  cospi  16027  efipi  16028  sin2pi  16030  cos2pi  16031  ef2pi  16032  cosq14gt0  16059  coseq00topi  16062  coseq0negpitopi  16063  sincos4thpi  16067  sincos6thpi  16069  sincos3rdpi  16070  pigt3  16071  cos02pilt1  16079  ioocosf1o  16082  dfrelog  16089  relogf1o  16090  relogcl  16091  relogiso  16103  logfac  16126  rpcxpsqrt  16157  rpabscxpbnd  16175  2logb9irr  16207  2logb9irrALT  16210  sqrt2cxp2logb9e3  16211  2irrexpq  16212  2logb9irrap  16213  2irrexpqap  16214  log2tlbndlog2  16220  log2ublem2  16222  log2ublem3  16223  log2ublog2  16224  birthdaylog2  16228  prmdvdsfi  16243  ppiqp1le  16267  ppi1  16270  cht1  16271  cht2  16276  ppiqnncl  16278  chtqrpcl  16279  ppiqeq0  16280  ppiqltx  16281  prmorcht  16282  mpodvdsmulf1o  16284  fsumdvdsmul  16285  ppiublem1  16291  ppiublem2  16292  ppiqub  16293  chtublem  16295  chtqub  16296  perfectlem2  16300  bclbnd  16307  bpos1lem  16309  bposlem4  16314  bposlem5  16315  bposlem6  16316  bposlem7  16317  bposlem8  16318  bposlem9  16319  lgsdir2lem1  16352  lgsdir2lem2  16353  lgsdir2lem4  16355  lgsdir2lem5  16356  lgsdi  16361  gausslemma2dlem0i  16381  gausslemma2dlem4  16388  lgseisenlem4  16397  lgsquadlem1  16401  lgsquad2lem2  16406  lgsquad2  16407  m1lgs  16409  2lgs2  16426  2lgslem4  16427  2lgsoddprmlem2  16430  2lgsoddprmlem3c  16433  2lgsoddprmlem3d  16434  2sqlem9  16448  2sqlem10  16449  1vgrex  16466  vtxval0  16499  iedgval0  16500  uhgr0  16531  upgrfi  16548  umgrislfupgrdom  16577  ausgrusgrben  16614  uspgredgiedg  16624  uspgriedgedg  16625  usgrislfuspgrdom  16636  uspgredg2vlem  16666  uspgredg2v  16667  usgr0  16685  griedg0prc  16696  subupgr  16719  vdegp1cid  16762  0wlk0  16817  clwwlkn1  16864  clwwlkn2  16867  eupth2lem1  16904  eulerpathum  16927  konigsbergiedgwen  16930  konigsberglem1  16934  konigsberglem3  16936  konigsberglem4  16937  konigsberglem5  16938  konigsberg  16939  ex-fl  16944  ex-ceil  16945  ex-exp  16946  ex-fac  16947  ex-gcd  16950  bj-stfal  16975  bj-stst  16978  bj-dcfal  16988  bj-dcdc  16992  bj-stdc  16993  bj-dcst  16994  bj-el2oss1o  17007  elabf2  17015  bd0  17055  bdeli  17077  bdcriota  17114  bdbm1.3ii  17122  bdinex1  17130  bdssexi  17134  bj-inex  17138  bj-snex  17144  bj-sucex  17154  bj-d0clsepcl  17156  bj-omind  17165  bj-om  17168  bj-2inf  17169  bj-peano2  17170  bdpeano5  17174  bj-omssonALT  17194  bj-inf2vnlem1  17201  bj-omex2  17208  bj-nn0sucALT  17209  3dom  17223  012of  17228  2o01f  17229  subctctexmid  17235  pw1dceq  17240  exmidpeirce  17243  wexmiddc  17247  wexmiddiffilem  17248  wexmiddifxylem  17250  wexmiddifxy  17251  nninfall  17258  nninfsellemqall  17264  nninfsellemeqinf  17265  nninfomnilem  17267  nninfomni  17268  exmidsbthrlem  17273  sbthom  17277  isomninnlem  17285  isomninn  17286  cvgcmp2nlemabs  17287  iooreen  17290  trilpolemisumle  17294  trilpolemeq1  17296  trilpo  17299  trirec0  17300  apdifflemr  17303  qdiff  17305  iswomninnlem  17306  iswomninn  17307  ismkvnnlem  17309  ismkvnn  17310  redcwlpo  17312  dcapnconst  17318  nconstwlpolem0  17320  nconstwlpo  17323  neapmkv  17325  neap0mkv  17326  taupi  17330