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  1807  equveli  1808  sbid  1823  sbieh  1839  exdistrfor  1849  dveeq2or  1865  ax11v  1876  ax11ev  1877  equs5or  1879  sb4or  1882  sb4bor  1884  nfsb2or  1886  sbequilem  1887  sbequi  1888  speiv  1911  nfsbxy  1998  nfsbxyt  1999  sbco  2024  sbcocom  2026  sbcomxyyz  2028  sbal1yz  2057  dvelimALT  2066  dvelimfv  2067  dvelimor  2074  eumoi  2115  moani  2153  elsb1  2212  elsb2  2213  eqeq1i  2242  eqeq2i  2245  eleq1i  2300  eleq2i  2301  nfcrii  2379  neeq1i  2429  neeq2i  2430  necon3i  2462  rspec  2596  rgen2a  2598  mprg  2601  r19.21  2620  r19.23  2653  raleqi  2747  rexeqi  2748  rabeqif  2806  elv  2819  elexi  2828  ceqsal  2845  vtocl3  2873  vtoclef  2892  vtocle  2893  spcv  2913  spcev  2914  clel3  2955  elabf  2963  elab2  2968  elab3  2972  euxfrdc  3006  reueq  3019  rmoimi2  3023  sbsbc  3049  sbc8g  3053  sbc6  3071  sbcie  3080  sbcrex  3125  csbvarg  3169  csbief  3186  csbie2  3191  sbnfc2  3202  sseli  3238  sselii  3239  sseq1i  3268  sseq2i  3269  difeq1i  3337  difeq2i  3338  uneq1i  3373  uneq2i  3374  ineq1i  3422  ineq2i  3423  ssinss1  3454  difdif2ss  3482  n0ii  3521  ne0ii  3522  vn0  3523  vn0m  3524  abf  3556  disj2  3568  difid  3581  0dif  3584  disjdif  3585  difin0  3587  undif1ss  3588  difdifdirss  3598  iftruei  3632  iffalsei  3635  ifbieq2i  3650  ifbieq12i  3652  pweqi  3678  sspwi  3688  pwid  3692  sneqi  3706  elsn  3710  elpr  3715  elsn2  3728  ralsn  3737  rexsn  3738  eltp  3742  rabrsndc  3764  preq1i  3776  preq2i  3777  prid1  3802  snnz  3816  snm  3817  prnz  3820  prm  3821  tpnz  3823  snss  3834  snsssn  3870  opeq1i  3891  opeq2i  3892  unieqi  3929  unissi  3942  inteqi  3958  intmin2  3980  intab  3983  intsn  3989  iinconstm  4005  iuniin  4006  iinss1  4008  iunxdif2  4045  ssiinf  4046  iinss  4048  iinss2  4049  iinab  4058  iundif2ss  4062  iindif2m  4064  iinin2m  4065  iunxsn  4073  iunxprg  4077  iinpw  4087  invdisjrab  4108  sndisj  4110  disjxsn  4112  breqi  4120  breq1i  4121  breq2i  4122  brab1  4162  opabbii  4182  truni  4227  bm1.3ii  4236  a9evsep  4237  ax9vsep  4238  zfnuleu  4239  axnul  4240  ssexi  4253  difexi  4258  rabex  4261  rabex2  4263  elpw2  4274  pwnss  4277  iin0r  4287  intv  4288  pwex  4301  snex  4303  notnotsnex  4305  ord3ex  4308  dtruarb  4309  undifexmid  4311  intid  4345  opnzi  4356  copsexg  4365  opwo0id  4370  opelopabf  4398  epelc  4417  elon  4500  inton  4519  onn0  4526  onm  4527  elsuc  4532  elsuc2  4533  sucid  4543  iunsuc  4546  onordi  4552  ontrci  4553  onelssi  4555  eusvnf  4579  ssonunii  4616  sucex  4626  onssi  4642  onsuci  4643  ordtriexmidlem  4646  ordtriexmidlem2  4647  ordtriexmid  4648  ontriexmidim  4649  ordtri2orexmid  4650  2ordpr  4651  ontr2exmid  4652  onsucsssucexmid  4654  onsucelsucexmid  4657  regexmidlemm  4659  reg2exmid  4663  onirri  4670  ruALT  4678  onprc  4679  sucon  4680  dtru  4687  0elsucexmid  4692  ordpwsucexmid  4697  ordtri2or2exmid  4698  ontri2orexmidim  4699  dcextest  4708  omex  4720  find  4726  omelon  4736  nnoni  4738  limom  4741  nnregexmid  4748  omsinds  4749  xpeq1i  4774  xpeq2i  4775  0nelxp  4782  opthprc  4806  mosubop  4821  releqi  4838  relssi  4846  relin1  4875  relin2  4876  reldif  4877  inopab  4892  difopab  4893  xpiindim  4897  opabbi2dv  4909  ideq  4912  coeq1i  4919  coeq2i  4920  cnveqi  4935  eldm  4958  eldm2  4959  dmeqi  4962  dmv  4977  rneqi  4990  elrnmpti  5015  dmex  5029  rnex  5030  reseq1i  5039  reseq2i  5040  residm  5075  resex  5084  resmpt3  5092  imaeq1i  5103  imaeq2i  5104  elima  5111  imaex  5121  elimasn  5134  args  5136  epini  5138  dfse2  5140  eliniseg2  5147  relbrcnv  5148  cotr  5149  issref  5150  cnvsym  5151  asymref  5153  intirr  5154  codir  5156  qfto  5157  ssrnres  5210  cnveq0  5224  cnvsn0  5236  dmsnop  5241  rnsnop  5248  resdm2  5258  dfco2a  5268  cocnvcnv1  5278  coi2  5284  coires1  5285  cnvssrndm  5289  cossxp  5290  cocnvres  5292  relrelss  5294  relcoi2  5298  unidmrn  5300  dfdm2  5302  unixpm  5303  cnvexg  5305  cnvex  5306  cnviinm  5309  iotaval  5329  funeqi  5378  funi  5389  funres  5398  funcnvsn  5406  funcnvcnv  5420  funin  5432  funcnvres  5434  isarep2  5448  fneq1i  5455  fneq2i  5456  fndmi  5461  fnresdisj  5473  fnresi  5481  mpt0  5491  dmmpti  5493  feq1i  5506  feq2i  5507  fdmi  5521  fun2  5542  fssres  5545  resasplitss  5549  fintm  5557  fconst6  5572  f1ores  5634  foimacnv  5637  resdif  5641  funcocnv2  5644  f10d  5655  f1ovi  5660  fveq1i  5676  fveq2i  5678  0fv  5713  fvun1  5748  fvopab3ig  5756  fvmptss2  5757  mptrcl  5765  elfvmptrab1  5777  fndmdif  5788  fneqeql2  5792  f1oresrab  5847  fmptco  5848  funopsn  5865  fnressn  5875  fressnfv  5876  fmptap  5879  fvsnun1  5886  fvsnun2  5887  fsnunfv  5890  fconst2  5906  mptex  5917  fnfvimad  5927  rinvf1o  6008  riotabiia  6030  acexmidlema  6049  acexmidlemb  6050  acexmidlemcase  6053  acexmidlem2  6055  acexmidlemv  6056  oveq1i  6068  oveq2i  6069  oveqi  6071  oprabidlem  6089  0neqopab  6106  oprabbii  6116  oprabss  6147  mpompt  6153  funoprab  6161  fnoprab  6164  ovigg  6182  elmpocl  6257  relmptopab  6264  resfunexgALT  6310  cofunexg  6311  mptexw  6315  opabex3d  6323  opabex3  6324  1st0  6351  2nd0  6352  op1st  6353  op2nd  6354  f1stres  6366  f2ndres  6367  fo1stresm  6368  fo2ndresm  6369  1stcof  6370  2ndcof  6371  1stexg  6374  2ndexg  6375  releldm2  6392  reldm  6393  dfoprab3  6398  mpomptsx  6406  mpompts  6407  fnmpoi  6412  dmmpo  6413  mpoexxg  6419  mpoexw  6422  1stconst  6430  2ndconst  6431  dfmpo  6432  algrflem  6438  algrflemg  6439  cnvoprab  6443  f1od2  6444  elmpom  6447  mpoxopn0yelv  6483  mpoxopoveq  6484  tposssxp  6493  brtpos2  6495  reldmtpos  6497  dftpos2  6505  dftpos4  6507  tpostpos  6508  tpostpos2  6509  tposfo  6515  tposf  6516  tposeqi  6521  tposex  6522  tposoprab  6524  issmo  6532  smores  6536  smores2  6538  iordsmo  6541  smo0  6542  tfrlem8  6562  tfrexlem  6578  tfr1onlem3  6582  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlemres  6593  tfri1dALT  6595  tfri2  6610  rdgisuc1  6628  rdg0  6631  frecfun  6639  frec0g  6641  freccllem  6646  frecfcllem  6648  frecsuclem  6650  frecrdg  6652  2on0  6670  xp01disj  6679  2oconcl  6685  fnoa  6693  oaexg  6694  fnom  6696  omexg  6697  fnoei  6698  oeiexg  6699  oei0  6705  oacl  6706  oasuc  6710  o1p1e2  6714  omsuc  6718  nna0r  6724  nnm0r  6725  1onn  6766  2onn  6767  3onn  6768  4onn  6769  2ssom  6770  eqerlem  6811  eceq2i  6818  elqs  6833  qsex  6839  ecqs  6844  iinerm  6854  th3qlem1  6884  th3q  6887  mapsn  6938  mapsnf1o3  6945  ixpiinm  6972  ixpssmap  6980  brdom  7000  f1dom  7012  enref  7017  dom2  7027  idssen  7029  ssdomg  7031  ensymi  7035  ensn1  7049  fiprc  7070  1domsn  7081  dom1o  7082  xpcomf1o  7089  xpcomco  7090  dom0  7104  0dom  7105  xpmapenlem  7115  phplem2  7120  php5  7125  snnen2og  7126  1nen2  7128  php5dom  7130  ssfilem  7143  ssfiexmid  7144  ssfilemd  7145  ssfiexmidt  7146  domfiexmid  7148  0fi  7154  diffitest  7157  findcard  7158  findcard2  7159  findcard2s  7160  isinfinf  7167  ac6sfi  7168  inffiexmid  7179  pw1fin  7183  unfiexmid  7191  xpfi  7205  fisseneq  7208  ssfirab  7210  residfi  7220  mapfi  7227  en1eqsn  7231  snexxph  7233  sbthlem2  7241  sbthlemi3  7242  sbthlemi6  7245  sbthlem7  7246  fi0  7275  fipwfi  7285  supeq1i  7292  infeq1i  7317  djuexb  7348  djuf1olemr  7358  inresflem  7364  djuinr  7367  updjudhcoinlf  7384  updjudhcoinrg  7385  casefun  7389  caserel  7391  caseinj  7393  caseinl  7395  caseinr  7396  omp1eomlem  7398  endjusym  7400  difinfsn  7404  difinfinf  7405  djuinj  7410  0ct  7411  ctmlemr  7412  ctssdclemn0  7414  ctssdccl  7415  omct  7421  ctfoex  7422  finomni  7444  exmidomni  7446  fodjuomni  7453  ctssexmid  7454  fodjumkv  7464  nninfwlporlem  7477  nninfwlpoimlemg  7479  nninfwlpoim  7483  nninfinfwlpo  7484  card0  7497  ficardon  7498  exmidonfinlem  7509  dju1p1e2  7513  exmidfodomrlemim  7517  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  iftrueb01  7546  3nelsucpw1  7557  sucpw1nss3  7558  3nsssucpw1  7559  fmelpw1o  7570  2onetap  7585  exmidmotap  7591  0npi  7644  dmaddpi  7656  dmmulpi  7657  1lt2pi  7671  0nnq  7695  1nq  7697  dmaddpq  7710  dmmulpq  7711  rec1nq  7726  1lt2nq  7737  halfnqq  7741  prarloclemarch2  7750  enq0enq  7762  nqnq0pi  7769  nnnq0lem1  7777  addnnnq0  7780  mulnnnq0  7781  nq0m0r  7787  addpinq1  7795  prarloclem5  7831  prarloclemcalc  7833  1pr  7885  1idprl  7921  1idpru  7922  ltexprlemm  7931  recexprlem1ssl  7964  recexprlem1ssu  7965  suplocexprlemell  8044  suplocexprlem2b  8045  suplocexprlemmu  8049  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  suplocexprlemlub  8055  prsrlem1  8073  addsrpr  8076  mulsrpr  8077  gt0srpr  8079  0nsr  8080  0r  8081  1sr  8082  m1r  8083  m1m1sr  8092  caucvgsr  8133  suplocsrlempr  8138  addresr  8168  mulresr  8169  pitonnlem1  8176  peano1nnnn  8183  axi2m1  8206  axcnre  8212  peano5nnnn  8223  axcaucvg  8231  mpomulf  8280  mulridi  8292  mullidi  8293  pnfnre  8331  mnfnre  8332  pnfnemnf  8344  mnfxr  8346  rexri  8347  ltnri  8382  ltleii  8392  00id  8430  addridi  8431  addlidi  8432  0cnALT  8479  negeqi  8483  negicn  8490  neg0  8535  renegcli  8551  negcli  8557  negidi  8558  negnegi  8559  subidi  8560  subid1i  8561  negne0bi  8562  negrebi  8563  mul02i  8680  mul01i  8681  mulm1i  8693  leidi  8776  gt0ne0ii  8778  inelr  8875  msqge0i  8908  gt0ap0ii  8919  1div1e1  8995  div1i  9031  eqnegi  9032  recclapi  9033  recidapi  9034  divmulapi  9057  rerecclapi  9068  redivclapi  9070  rerecapb  9134  recgt0  9141  ltp1i  9196  divgt0ii  9210  ltmul1ii  9219  ltdiv1ii  9220  sup3exmid  9248  peano5nni  9257  nnrei  9263  1nn  9265  nngt0i  9284  neg1ap0  9363  2timesi  9384  times2i  9385  2nn  9416  3nn  9417  4nn  9418  5nn  9419  6nn  9420  7nn  9421  8nn  9422  9nn  9423  2muline0  9480  rehalfcli  9504  nn0ssre  9517  nnnn0i  9521  dfn2  9526  0nn0  9528  nn0ge0i  9540  zrei  9600  neg1z  9626  nn0negzi  9629  dfz2  9667  nneoi  9700  peano5uzi  9705  dfuzi  9706  nn0ind-raph  9713  deceq1i  9733  deceq2i  9734  10nn  9742  numltc  9752  eluzel2  9876  eluz1i  9879  nn0uz  9907  nnuz  9908  uzuzle35  9915  infrenegsupex  9944  lbzbi  9966  divfnzn  9971  qdivcl  9993  irrmul  9997  irrmulap  9998  cnref1o  10001  0ltpnf  10134  mnflt0  10136  0lepnf  10142  xrltnsym  10145  xrlttri3  10149  nltpnft  10166  ngtmnft  10169  xrrebnd  10171  xnegmnf  10181  xneg0  10183  xltnegi  10187  xaddmnf1  10200  xaddmnf2  10201  mnfaddpnf  10203  xaddid1  10214  xnn0lenn0nn0  10217  xnn0xadd0  10219  xposdif  10234  ixxex  10251  iooval2  10267  unirnioo  10325  ioorebasg  10327  elrege0  10328  fzval2  10364  fzen  10397  fzprval  10438  fztpval  10439  uzdisj  10449  ige2m1fz  10466  fz01or  10467  fz1ssfz0  10473  fz0sn  10477  fz0tp  10478  fz0to3un2pr  10479  fz0to4untppr  10480  nn0disj  10494  1fv  10495  4fvwrd4  10496  fzo0ss1  10532  fzo01  10583  fzo12sn  10584  fzo0to2pr  10585  fzo0to3tp  10586  fzo0to42pr  10587  zsupssdc  10622  qbtwnxr  10641  flval  10656  fldiv4lem1div2  10691  modqfrac  10723  modqmulnn  10728  q2txmodxeq0  10770  frecuzrdgdom  10804  frecuzrdgfun  10806  frecuzrdgsuct  10810  frechashgf1o  10814  nnct  10821  xnn0nnen  10823  fxnn0nninf  10825  0tonninf  10826  1tonninf  10827  iseqvalcbv  10845  ser0f  10920  0exp0e1  10930  qexpcl  10941  qexpclz  10946  m1expcl2  10947  1exp  10954  sqvali  11005  sqcli  11006  sqeq0i  11007  resqcli  11010  sq1  11019  neg1sqe1  11020  iexpcyc  11030  qsqeqor  11036  facnn  11114  fac0  11115  fac1  11116  fac2  11118  fac3  11119  fac4  11120  bcval  11136  bcm1k  11147  bcpasc  11153  bccl  11154  4bc3eq4  11161  4bc2eq6  11162  hashinfom  11166  hashennn  11168  hashfz1  11171  fihasheq0  11181  hash0  11184  hashsng  11186  fihashen1  11187  en1hash  11188  omgadd  11191  hashp1i  11200  hashxp  11216  hashpwfi  11218  fimaxq  11219  ssenneg  11229  hashfibc  11232  zfz1iso  11238  hash2en  11240  wrdexi  11262  wrdv  11265  wrdeqi  11272  wrd0  11274  lsw0  11297  ccatclab  11307  ccatidid  11323  s1prc  11336  ccat1st1st  11354  swrds1  11385  fnpfx  11394  swrdccatin2  11446  pfxccatin12lem2  11448  cats1fvn  11481  shftidt2  11542  cjexp  11603  re0  11605  im0  11606  re1  11607  im1  11608  cj0  11611  cji  11612  recli  11621  imcli  11622  cjcli  11623  replimi  11624  cjcji  11625  reim0bi  11626  rerebi  11627  cjrebi  11628  recji  11629  imcji  11630  cjmulrcli  11631  cjmulvali  11632  cjmulge0i  11633  renegi  11634  imnegi  11635  cjnegi  11636  addcji  11637  uzin2  11697  rexanuz  11698  rexfiuz  11699  sqrtrval  11710  sqrt0  11714  resqrexlemcalc3  11726  resqrexlemcvg  11729  resqrex  11736  abs0  11768  absi  11769  qabsor  11785  absimle  11794  recan  11819  caubnd2  11827  leabsi  11838  absrei  11839  sqrtpclii  11840  sqrtgt0ii  11841  absvalsqi  11850  absvalsq2i  11851  abscli  11852  absge0i  11853  absval2i  11854  abs00i  11855  absgt0api  11856  absnegi  11857  abscji  11858  releabsi  11859  infxrnegsupex  11973  xrbdtri  11986  cbvsum  12070  sumeq1i  12073  sum0  12099  isumz  12100  fisumss  12103  fsumsersdc  12106  fsumadd  12117  isumclim  12132  isumclim3  12134  fsumcnv  12148  modfsummodlem1  12167  fsumrelem  12182  binomlem  12194  binom  12195  arisum2  12210  expcnv  12215  0.999...  12232  prodf1f  12254  cbvprod  12269  prodeq1i  12272  zproddc  12290  zprodap0  12292  prod0  12296  fprodssdc  12301  prodsnf  12303  fprodcnv  12336  fprodge0  12348  fprodge1  12350  ef0lem  12371  esum  12373  ere  12381  ege2le3  12382  ef0  12383  eff2  12391  efsep  12402  reeff1  12411  sin0  12440  cos0  12441  ef01bndlem  12467  cos2bnd  12471  sincos1sgn  12476  sincos2sgn  12477  sin4lt0  12478  eirr  12490  0dvds  12522  dvds1  12564  z0even  12622  n2dvdsm1  12624  z2even  12625  n2dvds3  12626  ndvdssub  12641  ndvdsi  12644  flodddiv4  12647  bits0  12659  bitsfzo  12666  0bits  12670  m1bits  12671  bitsinv1lem  12672  bitsinv1  12673  gcddvds  12684  gcd1  12708  6gcd4e2  12716  bezoutlembi  12726  dfgcd3  12731  dfgcd2  12735  nninfctlemfo  12761  nninfct  12762  3lcm2e6woprm  12808  qredeu  12819  isprm2lem  12838  isprm3  12840  prm2orodd  12848  isprm5lem  12863  sqrt2irr0  12886  pw2dvds  12888  phicl2  12936  phi1  12941  dfphi2  12942  phiprmpw  12944  eulerthlemrprm  12951  eulerthlemh  12953  odzval  12964  oddprm  12982  pczpre  13020  pcdiv  13025  pc0  13027  pcqdiv  13030  pcrec  13031  pcexp  13032  pcxcl  13034  pcxqcl  13035  pcdvdstr  13050  pc2dvds  13053  dvdsprmpweqnn  13059  pcmpt  13066  qexpz  13075  pockthi  13081  1arith2  13091  4sqlemffi  13119  4sqlem11  13124  4sqlem13m  13126  4sqlem19  13132  dec2dvds  13134  dec5nprm  13137  modxai  13139  modxp1i  13141  numexp0  13145  numexp1  13146  ballotfilem1  13164  ballotfilemonn  13165  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilem4  13185  ballotfilemi  13187  ballotfilem7  13223  ballotfilem8  13224  ballotfilemth  13225  ennnfonelemp1  13241  ennnfonelem1  13242  ennnfonelemkh  13247  ennnfonelemex  13249  ennnfonelemnn0  13257  ennnfonelemr  13258  exmidunben  13261  ctinfomlemom  13262  ctinfom  13263  ctinf  13265  qnnen  13266  omctfn  13278  omiunct  13279  ssnnctlemct  13281  nninfdc  13288  structcnvcnv  13312  structfun  13314  structfn  13315  ndxarg  13319  ndxid  13320  setsresg  13334  setsslnid  13348  basmex  13356  basmexd  13357  strleun  13401  strle1g  13403  prdsvallem  13564  imasaddfnlemg  13578  quslem  13588  xpsfrnel  13608  xpsff1o  13613  ismgmn0  13621  fn0g  13638  0g0  13639  fngsum  13651  idghm  14012  gfsumsn  14107  gfsumcl  14110  prdsex  14114  prdsval  14115  prdsbaslemss  14116  rhmfn  14417  rmodislmodlem  14624  rmodislmod  14625  lidlmex  14749  mopnset  14826  cntopex  14828  cnfldex  14833  cnfldbas  14834  mpocnfldadd  14835  mpocnfldmul  14837  cnfldcj  14839  cnfldtset  14840  cnfldle  14841  cnfldds  14842  cnring  14844  cnfld0  14845  cnfld1  14846  cnfldneg  14847  cnfldplusf  14848  cnfldsub  14849  cnfldmulg  14850  cnfldexp  14851  cnsubglem  14853  cnsubrglem  14854  gzsubrg  14856  gsumfzfsumlem0  14860  cnfldui  14863  zringring  14867  zringabl  14868  zringgrp  14869  zring1  14875  zringsubgval  14879  expghmap  14881  znval  14910  znle  14911  znbaslemnn  14913  znbas  14918  znzrh2  14920  znzrhval  14921  znzrhfo  14922  znleval  14927  znidom  14931  znidomb  14932  fnpsr  14941  psrelbas  14956  psradd  14960  psraddcl  14961  psr1clfi  14969  mplrcl  14975  mplbasss  14977  mpladd  14985  istopon  15004  topontopi  15007  toponunii  15008  toponrestid  15012  istps  15023  topontopn  15028  eltpsi  15032  eltg4i  15046  eltg3  15048  tg1  15050  tg2  15051  tgclb  15056  topnex  15077  sn0topon  15079  distps  15082  cldrcl  15093  sn0cld  15128  restco  15165  lmrcl  15183  ssidcn  15201  cnconst2  15224  cnptopresti  15229  cnptoprest  15230  txuni2  15247  txbas  15249  eltx  15250  txcnp  15262  upxp  15263  txcnmpt  15264  uptx  15265  txcn  15266  txrest  15267  txlm  15270  cnmptid  15272  cnmpt1st  15279  cnmpt2nd  15280  hmeofn  15293  psmetge0  15322  ismeti  15337  xmetunirn  15349  xmetge0  15356  unirnblps  15413  unirnbl  15414  mopnex  15496  qtopbasss  15512  retop  15515  uniretop  15516  iooretopg  15519  cnxmet  15522  cntoptopon  15523  cnbl0  15525  cnfldxms  15528  cnfldtps  15529  rexmet  15540  blssioo  15544  tgioo  15545  tgqioo  15546  cnopnap  15602  hovercncf  15637  limcresi  15657  dvfvalap  15672  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvcnp2cntop  15690  dvcoapbr  15698  dvexp2  15703  dvrecap  15704  dveflem  15717  dvef  15718  plyun0  15727  plyrecj  15754  dvply2  15758  reeff1o  15764  sin0pilem1  15772  sin0pilem2  15773  pilem3  15774  pigt2lt4  15775  pire  15777  sinhalfpilem  15782  pidiv2halves  15786  cosneghalfpi  15789  cospi  15791  efipi  15792  sin2pi  15794  cos2pi  15795  ef2pi  15796  cosq14gt0  15823  coseq00topi  15826  coseq0negpitopi  15827  sincos4thpi  15831  sincos6thpi  15833  sincos3rdpi  15834  pigt3  15835  cos02pilt1  15842  ioocosf1o  15845  dfrelog  15851  relogf1o  15852  relogcl  15853  relogiso  15864  rpcxpsqrt  15913  rpabscxpbnd  15931  2logb9irr  15962  2logb9irrALT  15965  sqrt2cxp2logb9e3  15966  2irrexpq  15967  2logb9irrap  15968  2irrexpqap  15969  mpodvdsmulf1o  15984  fsumdvdsmul  15985  perfectlem2  15994  lgsdir2lem1  16027  lgsdir2lem2  16028  lgsdir2lem4  16030  lgsdir2lem5  16031  lgsdi  16036  gausslemma2dlem0i  16056  gausslemma2dlem4  16063  lgseisenlem4  16072  lgsquadlem1  16076  lgsquad2lem2  16081  lgsquad2  16082  m1lgs  16084  2lgs2  16101  2lgslem4  16102  2lgsoddprmlem2  16105  2lgsoddprmlem3c  16108  2lgsoddprmlem3d  16109  2sqlem9  16123  2sqlem10  16124  1vgrex  16141  vtxval0  16174  iedgval0  16175  uhgr0  16206  upgrfi  16223  umgrislfupgrdom  16252  ausgrusgrben  16289  uspgredgiedg  16299  uspgriedgedg  16300  usgrislfuspgrdom  16311  uspgredg2vlem  16341  uspgredg2v  16342  usgr0  16360  griedg0prc  16371  subupgr  16394  vdegp1cid  16437  0wlk0  16492  clwwlkn1  16539  clwwlkn2  16542  eupth2lem1  16579  eulerpathum  16602  konigsbergiedgwen  16605  konigsberglem1  16609  konigsberglem3  16611  konigsberglem4  16612  konigsberglem5  16613  konigsberg  16614  ex-fl  16619  ex-ceil  16620  ex-exp  16621  ex-fac  16622  ex-gcd  16625  bj-stfal  16640  bj-stst  16643  bj-dcfal  16653  bj-dcdc  16657  bj-stdc  16658  bj-dcst  16659  bj-el2oss1o  16672  elabf2  16680  bd0  16720  bdeli  16742  bdcriota  16779  bdbm1.3ii  16787  bdinex1  16795  bdssexi  16799  bj-inex  16803  bj-snex  16809  bj-sucex  16819  bj-d0clsepcl  16821  bj-omind  16830  bj-om  16833  bj-2inf  16834  bj-peano2  16835  bdpeano5  16839  bj-omssonALT  16859  bj-inf2vnlem1  16866  bj-omex2  16873  bj-nn0sucALT  16874  3dom  16888  012of  16893  2o01f  16894  subctctexmid  16900  pw1dceq  16904  exmidpeirce  16907  nninfall  16913  nninfsellemqall  16919  nninfsellemeqinf  16920  nninfomnilem  16922  nninfomni  16923  exmidsbthrlem  16928  sbthom  16932  isomninnlem  16940  isomninn  16941  cvgcmp2nlemabs  16942  iooreen  16945  trilpolemisumle  16948  trilpolemeq1  16950  trilpo  16953  trirec0  16954  apdifflemr  16957  qdiff  16959  iswomninnlem  16960  iswomninn  16961  ismkvnnlem  16963  ismkvnn  16964  redcwlpo  16966  dcapnconst  16973  nconstwlpolem0  16975  nconstwlpo  16978  neapmkv  16980  neap0mkv  16981  taupi  16985