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 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	|- 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 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  6515  mpoxopoveq  6516  tposssxp  6525  brtpos2  6527  reldmtpos  6529  dftpos2  6537  dftpos4  6539  tpostpos  6540  tpostpos2  6541  tposfo  6547  tposf  6548  tposeqi  6553  tposex  6554  tposoprab  6556  issmo  6564  smores  6568  smores2  6570  iordsmo  6573  smo0  6574  tfrlem8  6594  tfrexlem  6610  tfr1onlem3  6614  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlemres  6625  tfri1dALT  6627  tfri2  6642  rdgisuc1  6660  rdg0  6663  frecfun  6671  frec0g  6673  freccllem  6678  frecfcllem  6680  frecsuclem  6682  frecrdg  6684  2on0  6702  xp01disj  6711  2oconcl  6717  fnoa  6725  oaexg  6726  fnom  6728  omexg  6729  fnoei  6730  oeiexg  6731  oei0  6737  oacl  6738  oasuc  6742  o1p1e2  6746  omsuc  6750  nna0r  6756  nnm0r  6757  1onn  6798  2onn  6799  3onn  6800  4onn  6801  2ssom  6802  eqerlem  6843  eceq2i  6850  elqs  6865  qsex  6871  ecqs  6876  iinerm  6886  th3qlem1  6916  th3q  6919  mapsn  6978  mapsnf1o3  6985  ixpiinm  7012  ixpssmap  7020  brdom  7040  f1dom  7052  enref  7057  dom2  7067  idssen  7069  ssdomg  7071  ensymi  7075  ensn1  7089  fiprc  7110  1domsn  7121  dom1o  7122  xpcomf1o  7129  xpcomco  7130  dom0  7144  0dom  7145  xpmapenlem  7155  phplem2  7160  php5  7165  snnen2og  7166  1nen2  7168  php5dom  7170  ssfilem  7183  ssfiexmid  7184  ssfilemd  7185  ssfiexmidt  7186  domfiexmid  7188  0fi  7194  diffitest  7197  findcard  7198  findcard2  7199  findcard2s  7200  isinfinf  7207  ac6sfi  7208  inffiexmid  7219  pw1fin  7223  unfiexmid  7231  xpfi  7245  fisseneq  7248  ssfirab  7250  residfi  7260  mapfi  7267  en1eqsn  7272  snexxph  7274  sbthlem2  7282  sbthlemi3  7283  sbthlemi6  7286  sbthlem7  7287  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  9659  neg1z  9685  nn0negzi  9688  dfz2  9726  nneoi  9760  peano5uzi  9765  dfuzi  9766  nn0ind-raph  9773  deceq1i  9793  deceq2i  9794  10nn  9806  numltc  9817  eluzel2  9941  eluz1i  9944  nn0uz  9972  nnuz  9973  uzuzle35  9980  infrenegsupex  10009  lbzbi  10031  divfnzn  10036  qdivcl  10058  irrmul  10063  irrmulap  10064  cnref1o  10067  0ltpnf  10200  mnflt0  10202  0lepnf  10208  xrltnsym  10211  xrlttri3  10215  nltpnft  10232  ngtmnft  10235  xrrebnd  10237  xnegmnf  10247  xneg0  10249  xltnegi  10253  xaddmnf1  10266  xaddmnf2  10267  mnfaddpnf  10269  xaddid1  10280  xnn0lenn0nn0  10283  xnn0xadd0  10285  xposdif  10300  ixxex  10317  iooval2  10333  unirnioo  10391  ioorebasg  10393  elrege0  10394  fzval2  10430  fzen  10463  fzprval  10505  fztpval  10506  uzdisj  10516  ige2m1fz  10533  fz01or  10534  fz1ssfz0  10540  fz0sn  10544  fz0tp  10545  fz0to3un2pr  10546  fz0to4untppr  10547  nn0disj  10561  1fv  10562  4fvwrd4  10563  fzo0ss1  10599  fzo01  10650  fzo12sn  10651  fzo0to2pr  10652  fzo0to3tp  10653  fzo0to42pr  10654  zsupssdc  10689  qbtwnxr  10708  flval  10723  flapcl  10727  flaplelt  10729  fldiv4lem1div2  10762  modqfrac  10794  modqmulnn  10799  q2txmodxeq0  10841  frecuzrdgdom  10875  frecuzrdgfun  10877  frecuzrdgsuct  10881  frechashgf1o  10885  nnct  10892  xnn0nnen  10894  fxnn0nninf  10896  0tonninf  10897  1tonninf  10898  iseqvalcbv  10916  ser0f  10991  0exp0e1  11001  qexpcl  11012  qexpclz  11017  m1expcl2  11018  1exp  11025  sqvali  11076  sqcli  11077  sqeq0i  11078  resqcli  11081  sq1  11090  neg1sqe1  11091  iexpcyc  11101  qsqeqor  11107  nn0sqdc  11167  facnn  11186  fac0  11187  fac1  11188  fac2  11190  fac3  11191  fac4  11192  bcval  11208  bcm1k  11219  bcpasc  11225  bccl  11226  4bc3eq4  11233  4bc2eq6  11234  hashinfom  11238  hashennn  11240  hashfz1  11243  fihasheq0  11253  hash0  11256  hashsng  11258  fihashen1  11259  en1hash  11260  omgadd  11263  hashp1i  11272  hashxp  11288  hashpwfi  11290  fimaxq  11291  ssenneg  11301  hashfibc  11304  hashf1lem1  11306  hashf1  11308  zfz1iso  11314  hash2en  11316  wrdexi  11338  wrdv  11341  wrdeqi  11348  wrd0  11350  lsw0  11373  ccatclab  11383  ccatidid  11399  s1prc  11412  ccat1st1st  11430  swrds1  11461  fnpfx  11470  swrdccatin2  11522  pfxccatin12lem2  11524  cats1fvn  11557  shftidt2  11618  cjexp  11679  re0  11682  im0  11683  re1  11684  im1  11685  cj0  11688  cji  11689  recli  11698  imcli  11699  cjcli  11700  replimi  11701  cjcji  11702  reim0bi  11703  rerebi  11704  cjrebi  11705  recji  11706  imcji  11707  cjmulrcli  11708  cjmulvali  11709  cjmulge0i  11710  renegi  11711  imnegi  11712  cjnegi  11713  addcji  11714  uzin2  11774  rexanuz  11775  rexfiuz  11776  sqrtrval  11787  sqrt0  11791  resqrexlemcalc3  11803  resqrexlemcvg  11806  resqrex  11813  abs0  11845  absi  11846  qabsor  11862  absimle  11872  recan  11897  caubnd2  11905  leabsi  11916  absrei  11917  sqrtpclii  11918  sqrtgt0ii  11919  absvalsqi  11928  absvalsq2i  11929  abscli  11930  absge0i  11931  absval2i  11932  abs00i  11933  absgt0api  11934  absnegi  11935  abscji  11936  releabsi  11937  infxrnegsupex  12053  xrbdtri  12066  cbvsum  12150  sumeq1i  12153  sum0  12179  isumz  12180  fisumss  12183  fsumsersdc  12186  fsumadd  12197  isumclim  12212  isumclim3  12214  fsumcnv  12228  modfsummodlem1  12247  fsumrelem  12262  binomlem  12274  binom  12275  arisum2  12290  expcnv  12295  0.999...  12312  prodf1f  12334  cbvprod  12349  prodeq1i  12352  zproddc  12370  zprodap0  12372  prod0  12376  fprodssdc  12381  prodsnf  12383  fprodcnv  12416  fprodge0  12428  fprodge1  12430  ef0lem  12451  esum  12453  ere  12461  ege2le3  12462  ef0  12463  eff2  12471  efsep  12482  reeff1  12491  sin0  12520  cos0  12521  ef01bndlem  12547  cos2bnd  12551  sincos1sgn  12556  sincos2sgn  12557  sin4lt0  12558  eirr  12570  0dvds  12602  dvds1  12644  z0even  12702  n2dvdsm1  12704  z2even  12705  n2dvds3  12706  ndvdssub  12721  ndvdsi  12724  flodddiv4  12727  bits0  12739  bitsfzo  12746  0bits  12750  m1bits  12751  bitsinv1lem  12752  bitsinv1  12753  gcddvds  12764  gcd1  12788  6gcd4e2  12796  bezoutlembi  12806  dfgcd3  12811  dfgcd2  12815  nninfctlemfo  12841  nninfct  12842  3lcm2e6woprm  12888  qredeu  12899  isprm2lem  12918  isprm3  12920  prm2orodd  12928  isprm5lem  12944  sqrt2irr0  12967  sqrtrirr  13013  phicl2  13020  phi1  13025  dfphi2  13026  phiprmpw  13028  eulerthlemrprm  13035  eulerthlemh  13037  odzval  13048  oddprm  13066  pczpre  13104  pcdiv  13109  pc0  13111  pcqdiv  13114  pcrec  13115  pcexp  13116  pcxcl  13118  pcxqcl  13119  pcdvdstr  13134  pc2dvds  13137  dvdsprmpweqnn  13143  pcmpt  13150  qexpz  13159  pockthi  13165  1arith2  13175  4sqlemffi  13203  4sqlem11  13208  4sqlem13m  13210  4sqlem19  13216  dec2dvds  13218  dec5nprm  13221  modxai  13223  modxp1i  13225  mod2xnegi  13226  numexp0  13230  numexp1  13231  1259lem5  13274  ballotfilem1  13277  ballotfilemonn  13278  ballotfilem2  13285  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilem4  13298  ballotfilemi  13300  ballotfilem7  13336  ballotfilem8  13337  ballotfilemth  13338  ennnfonelemp1  13354  ennnfonelem1  13355  ennnfonelemkh  13360  ennnfonelemex  13362  ennnfonelemnn0  13370  ennnfonelemr  13371  exmidunben  13374  ctinfomlemom  13375  ctinfom  13376  ctinf  13378  qnnen  13379  omctfn  13391  omiunct  13392  ssnnctlemct  13394  nninfdc  13401  structcnvcnv  13425  structfun  13427  structfn  13428  ndxarg  13432  ndxid  13433  setsresg  13447  setsslnid  13461  basmex  13469  basmexd  13470  slotm  13472  strleun  13516  strle1g  13518  prdsvallem  13679  imasaddfnlemg  13693  quslem  13703  xpsfrnel  13723  xpsff1o  13728  ismgmn0  13736  fn0g  13753  0g0  13754  fngzsum  13766  idghm  14120  elcntr  14162  gsumsncmn  14245  gsumclfi  14248  gsummptfidmadd  14250  gsumsubmclfi  14252  gsummptfidmsplit  14253  gsumconstcmn  14265  gsum2dfilem2  14271  gsumcom2fi  14274  prdsex  14278  prdsval  14279  prdsbaslemss  14280  mgpplusg  14328  mgpbas  14331  ringidval  14371  rhmfn  14587  rmodislmodlem  14795  rmodislmod  14796  lidlmex  14920  mopnset  14997  cntopex  14999  cnfldex  15004  cnfldbas  15005  mpocnfldadd  15006  mpocnfldmul  15008  cnfldcj  15010  cnfldtset  15011  cnfldle  15012  cnfldds  15013  cnring  15015  cnfld0  15016  cnfld1  15017  cnfldneg  15018  cnfldplusf  15019  cnfldsub  15020  cnfldmulg  15021  cnfldexp  15022  cnsubglem  15024  cnsubrglem  15025  gzsubrg  15027  gsumfsum  15031  cnfldui  15032  zringring  15036  zringabl  15037  zringgrp  15038  zring1  15044  zringsubgval  15048  expghmap  15050  znval  15079  znle  15080  znbaslemnn  15082  znbas  15087  znzrh2  15089  znzrhval  15090  znzrhfo  15091  znleval  15096  znidom  15100  znidomb  15101  fnpsr  15161  psrass1filem  15186  psrelbas  15188  psradd  15192  psraddcl  15193  psrmulfval  15196  psr1clfi  15207  mplbas  15223  mplrcl  15227  mpladd  15237  istopon  15256  topontopi  15259  toponunii  15260  toponrestid  15264  istps  15275  topontopn  15280  eltpsi  15284  eltg4i  15298  eltg3  15300  tg1  15302  tg2  15303  tgclb  15308  topnex  15329  sn0topon  15331  distps  15334  cldrcl  15345  sn0cld  15380  restco  15417  lmrcl  15435  ssidcn  15453  cnconst2  15476  cnptopresti  15481  cnptoprest  15482  txuni2  15499  txbas  15501  eltx  15502  txcnp  15514  upxp  15515  txcnmpt  15516  uptx  15517  txcn  15518  txrest  15519  txlm  15522  cnmptid  15524  cnmpt1st  15531  cnmpt2nd  15532  hmeofn  15545  psmetge0  15574  ismeti  15589  xmetunirn  15601  xmetge0  15608  unirnblps  15665  unirnbl  15666  mopnex  15748  qtopbasss  15764  retop  15767  uniretop  15768  iooretopg  15771  cnxmet  15774  cntoptopon  15775  cnbl0  15777  cnfldxms  15780  cnfldtps  15781  rexmet  15792  blssioo  15796  tgioo  15797  tgqioo  15798  cnopnap  15854  hovercncf  15889  limcresi  15909  dvfvalap  15924  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvcnp2cntop  15942  dvcoapbr  15950  dvexp2  15955  dvrecap  15956  dveflem  15969  dvef  15970  plyun0  15979  plyrecj  16006  dvply2  16010  reeff1o  16016  sin0pilem1  16025  sin0pilem2  16026  pilem3  16027  pigt2lt4  16028  pire  16030  sinhalfpilem  16035  pidiv2halves  16039  cosneghalfpi  16042  cospi  16044  efipi  16045  sin2pi  16047  cos2pi  16048  ef2pi  16049  cosq14gt0  16076  coseq00topi  16079  coseq0negpitopi  16080  sincos4thpi  16084  sincos6thpi  16086  sincos3rdpi  16087  pigt3  16088  cos02pilt1  16096  ioocosf1o  16099  dfrelog  16106  relogf1o  16107  relogcl  16108  relogiso  16120  logfac  16143  rpcxpsqrt  16174  rpabscxpbnd  16192  2logb9irr  16224  2logb9irrALT  16227  sqrt2cxp2logb9e3  16228  2irrexpq  16229  2logb9irrap  16230  2irrexpqap  16231  log2tlbndlog2  16237  log2ublem2  16239  log2ublem3  16240  log2ublog2  16241  birthdaylog2  16245  prmdvdsfi  16260  ppiqp1le  16284  ppi1  16287  cht1  16288  cht2  16293  ppiqnncl  16295  chtqrpcl  16296  ppiqeq0  16297  ppiqltx  16298  prmorcht  16299  mpodvdsmulf1o  16301  fsumdvdsmul  16302  ppiublem1  16308  ppiublem2  16309  ppiqub  16310  chtublem  16312  chtqub  16313  perfectlem2  16317  bclbnd  16324  bpos1lem  16326  bposlem4  16331  bposlem5  16332  bposlem6  16333  bposlem7  16334  bposlem8  16335  bposlem9  16336  lgsdir2lem1  16369  lgsdir2lem2  16370  lgsdir2lem4  16372  lgsdir2lem5  16373  lgsdi  16378  gausslemma2dlem0i  16398  gausslemma2dlem4  16405  lgseisenlem4  16414  lgsquadlem1  16418  lgsquad2lem2  16423  lgsquad2  16424  m1lgs  16426  2lgs2  16443  2lgslem4  16444  2lgsoddprmlem2  16447  2lgsoddprmlem3c  16450  2lgsoddprmlem3d  16451  2sqlem9  16465  2sqlem10  16466  1vgrex  16483  vtxval0  16516  iedgval0  16517  uhgr0  16548  upgrfi  16565  umgrislfupgrdom  16594  ausgrusgrben  16631  uspgredgiedg  16641  uspgriedgedg  16642  usgrislfuspgrdom  16653  uspgredg2vlem  16683  uspgredg2v  16684  usgr0  16702  griedg0prc  16713  subupgr  16736  vdegp1cid  16779  0wlk0  16834  clwwlkn1  16881  clwwlkn2  16884  eupth2lem1  16921  eulerpathum  16944  konigsbergiedgwen  16947  konigsberglem1  16951  konigsberglem3  16953  konigsberglem4  16954  konigsberglem5  16955  konigsberg  16956  ex-fl  16961  ex-ceil  16962  ex-exp  16963  ex-fac  16964  ex-gcd  16967  bj-stfal  16992  bj-stst  16995  bj-dcfal  17005  bj-dcdc  17009  bj-stdc  17010  bj-dcst  17011  bj-el2oss1o  17024  elabf2  17032  bd0  17072  bdeli  17094  bdcriota  17131  bdbm1.3ii  17139  bdinex1  17147  bdssexi  17151  bj-inex  17155  bj-snex  17161  bj-sucex  17171  bj-d0clsepcl  17173  bj-omind  17182  bj-om  17185  bj-2inf  17186  bj-peano2  17187  bdpeano5  17191  bj-omssonALT  17211  bj-inf2vnlem1  17218  bj-omex2  17225  bj-nn0sucALT  17226  3dom  17240  012of  17245  2o01f  17246  subctctexmid  17252  pw1dceq  17257  exmidpeirce  17260  wexmiddc  17264  wexmiddiffilem  17265  wexmiddifxylem  17267  wexmiddifxy  17268  nninfall  17275  nninfsellemqall  17281  nninfsellemeqinf  17282  nninfomnilem  17284  nninfomni  17285  exmidsbthrlem  17290  sbthom  17294  isomninnlem  17302  isomninn  17303  cvgcmp2nlemabs  17304  iooreen  17307  trilpolemisumle  17311  trilpolemeq1  17313  trilpo  17316  trirec0  17317  apdifflemr  17320  qdiff  17322  iswomninnlem  17323  iswomninn  17324  ismkvnnlem  17326  ismkvnn  17327  redcwlpo  17329  dcapnconst  17335  nconstwlpolem0  17337  nconstwlpo  17340  neapmkv  17342  neap0mkv  17343  taupi  17347