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 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	⊢ 𝜑
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  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  2954  elabf  2962  elab2  2967  elab3  2971  euxfrdc  3005  reueq  3018  rmoimi2  3022  sbsbc  3048  sbc8g  3052  sbc6  3070  sbcie  3079  sbcrex  3124  csbvarg  3168  csbief  3185  csbie2  3190  sbnfc2  3201  sseli  3236  sselii  3237  sseq1i  3266  sseq2i  3267  difeq1i  3335  difeq2i  3336  uneq1i  3371  uneq2i  3372  ineq1i  3420  ineq2i  3421  ssinss1  3452  difdif2ss  3480  n0ii  3519  ne0ii  3520  vn0  3521  vn0m  3522  abf  3554  disj2  3566  difid  3579  0dif  3582  disjdif  3583  difin0  3585  undif1ss  3586  difdifdirss  3596  iftruei  3630  iffalsei  3633  ifbieq2i  3648  ifbieq12i  3650  pweqi  3675  sspwi  3685  pwid  3689  sneqi  3703  elsn  3707  elpr  3712  elsn2  3725  ralsn  3734  rexsn  3735  eltp  3739  rabrsndc  3761  preq1i  3773  preq2i  3774  prid1  3799  snnz  3813  snm  3814  prnz  3817  prm  3818  tpnz  3820  snss  3831  snsssn  3867  opeq1i  3888  opeq2i  3889  unieqi  3926  unissi  3939  inteqi  3955  intmin2  3977  intab  3980  intsn  3986  iinconstm  4002  iuniin  4003  iinss1  4005  iunxdif2  4042  ssiinf  4043  iinss  4045  iinss2  4046  iinab  4055  iundif2ss  4059  iindif2m  4061  iinin2m  4062  iunxsn  4070  iunxprg  4074  iinpw  4084  invdisjrab  4105  sndisj  4107  disjxsn  4109  breqi  4117  breq1i  4118  breq2i  4119  brab1  4159  opabbii  4179  truni  4224  bm1.3ii  4233  a9evsep  4234  ax9vsep  4235  zfnuleu  4236  axnul  4237  ssexi  4250  difexi  4255  rabex  4258  rabex2  4260  elpw2  4271  pwnss  4274  iin0r  4284  intv  4285  pwex  4298  snex  4300  notnotsnex  4302  ord3ex  4305  dtruarb  4306  undifexmid  4308  intid  4342  opnzi  4353  copsexg  4362  opwo0id  4367  opelopabf  4395  epelc  4414  elon  4497  inton  4516  onn0  4523  onm  4524  elsuc  4529  elsuc2  4530  sucid  4540  iunsuc  4543  onordi  4549  ontrci  4550  onelssi  4552  eusvnf  4576  ssonunii  4613  sucex  4623  onssi  4639  onsuci  4640  ordtriexmidlem  4643  ordtriexmidlem2  4644  ordtriexmid  4645  ontriexmidim  4646  ordtri2orexmid  4647  2ordpr  4648  ontr2exmid  4649  onsucsssucexmid  4651  onsucelsucexmid  4654  regexmidlemm  4656  reg2exmid  4660  onirri  4667  ruALT  4675  onprc  4676  sucon  4677  dtru  4684  0elsucexmid  4689  ordpwsucexmid  4694  ordtri2or2exmid  4695  ontri2orexmidim  4696  dcextest  4705  omex  4717  find  4723  omelon  4733  nnoni  4735  limom  4738  nnregexmid  4745  omsinds  4746  xpeq1i  4771  xpeq2i  4772  0nelxp  4779  opthprc  4803  mosubop  4818  releqi  4835  relssi  4843  relin1  4872  relin2  4873  reldif  4874  inopab  4889  difopab  4890  xpiindim  4894  opabbi2dv  4906  ideq  4909  coeq1i  4916  coeq2i  4917  cnveqi  4932  eldm  4955  eldm2  4956  dmeqi  4959  dmv  4974  rneqi  4987  elrnmpti  5012  dmex  5026  rnex  5027  reseq1i  5036  reseq2i  5037  residm  5072  resex  5081  resmpt3  5089  imaeq1i  5100  imaeq2i  5101  elima  5108  imaex  5118  elimasn  5131  args  5133  epini  5135  dfse2  5137  eliniseg2  5144  relbrcnv  5145  cotr  5146  issref  5147  cnvsym  5148  asymref  5150  intirr  5151  codir  5153  qfto  5154  ssrnres  5207  cnveq0  5221  cnvsn0  5233  dmsnop  5238  rnsnop  5245  resdm2  5255  dfco2a  5265  cocnvcnv1  5275  coi2  5281  coires1  5282  cnvssrndm  5286  cossxp  5287  cocnvres  5289  relrelss  5291  relcoi2  5295  unidmrn  5297  dfdm2  5299  unixpm  5300  cnvexg  5302  cnvex  5303  cnviinm  5306  iotaval  5326  funeqi  5375  funi  5386  funres  5395  funcnvsn  5403  funcnvcnv  5417  funin  5429  funcnvres  5431  isarep2  5445  fneq1i  5452  fneq2i  5453  fndmi  5458  fnresdisj  5470  fnresi  5478  mpt0  5488  dmmpti  5490  feq1i  5503  feq2i  5504  fdmi  5518  fun2  5539  fssres  5542  resasplitss  5546  fintm  5554  fconst6  5569  f1ores  5631  foimacnv  5634  resdif  5638  funcocnv2  5641  f10d  5652  f1ovi  5657  fveq1i  5673  fveq2i  5675  0fv  5710  fvun1  5745  fvopab3ig  5753  fvmptss2  5754  mptrcl  5762  elfvmptrab1  5774  fndmdif  5785  fneqeql2  5789  f1oresrab  5844  fmptco  5845  funopsn  5862  fnressn  5872  fressnfv  5873  fmptap  5876  fvsnun1  5883  fvsnun2  5884  fsnunfv  5887  fconst2  5903  mptex  5914  fnfvimad  5924  riotabiia  6024  acexmidlema  6043  acexmidlemb  6044  acexmidlemcase  6047  acexmidlem2  6049  acexmidlemv  6050  oveq1i  6062  oveq2i  6063  oveqi  6065  oprabidlem  6083  0neqopab  6100  oprabbii  6110  oprabss  6141  mpompt  6147  funoprab  6155  fnoprab  6158  ovigg  6176  elmpocl  6251  relmptopab  6258  resfunexgALT  6303  cofunexg  6304  mptexw  6308  opabex3d  6316  opabex3  6317  1st0  6340  2nd0  6341  op1st  6342  op2nd  6343  f1stres  6355  f2ndres  6356  fo1stresm  6357  fo2ndresm  6358  1stcof  6359  2ndcof  6360  1stexg  6363  2ndexg  6364  releldm2  6381  reldm  6382  dfoprab3  6387  mpomptsx  6395  mpompts  6396  fnmpoi  6401  dmmpo  6402  mpoexxg  6408  mpoexw  6411  1stconst  6419  2ndconst  6420  dfmpo  6421  algrflem  6427  algrflemg  6428  cnvoprab  6432  f1od2  6433  elmpom  6436  mpoxopn0yelv  6472  mpoxopoveq  6473  tposssxp  6482  brtpos2  6484  reldmtpos  6486  dftpos2  6494  dftpos4  6496  tpostpos  6497  tpostpos2  6498  tposfo  6504  tposf  6505  tposeqi  6510  tposex  6511  tposoprab  6513  issmo  6521  smores  6525  smores2  6527  iordsmo  6530  smo0  6531  tfrlem8  6551  tfrexlem  6567  tfr1onlem3  6571  tfr1onlemsucaccv  6574  tfr1onlembxssdm  6576  tfr1onlemres  6582  tfri1dALT  6584  tfri2  6599  rdgisuc1  6617  rdg0  6620  frecfun  6628  frec0g  6630  freccllem  6635  frecfcllem  6637  frecsuclem  6639  frecrdg  6641  2on0  6659  xp01disj  6668  2oconcl  6674  fnoa  6682  oaexg  6683  fnom  6685  omexg  6686  fnoei  6687  oeiexg  6688  oei0  6694  oacl  6695  oasuc  6699  o1p1e2  6703  omsuc  6707  nna0r  6713  nnm0r  6714  1onn  6755  2onn  6756  3onn  6757  4onn  6758  2ssom  6759  eqerlem  6800  eceq2i  6807  elqs  6822  qsex  6828  ecqs  6833  iinerm  6843  th3qlem1  6873  th3q  6876  mapsn  6927  mapsnf1o3  6934  ixpiinm  6961  ixpssmap  6969  brdom  6989  f1dom  7001  enref  7006  dom2  7016  idssen  7018  ssdomg  7020  ensymi  7024  ensn1  7038  fiprc  7059  1domsn  7070  dom1o  7071  xpcomf1o  7078  xpcomco  7079  dom0  7093  0dom  7094  xpmapenlem  7104  phplem2  7109  php5  7114  snnen2og  7115  1nen2  7117  php5dom  7119  ssfilem  7132  ssfiexmid  7133  ssfilemd  7134  ssfiexmidt  7135  domfiexmid  7137  0fi  7143  diffitest  7146  findcard  7147  findcard2  7148  findcard2s  7149  isinfinf  7156  ac6sfi  7157  inffiexmid  7168  pw1fin  7172  unfiexmid  7180  xpfi  7194  fisseneq  7197  ssfirab  7199  residfi  7209  mapfi  7216  en1eqsn  7220  snexxph  7222  sbthlem2  7230  sbthlemi3  7231  sbthlemi6  7234  sbthlem7  7235  fi0  7264  fipwfi  7274  supeq1i  7281  infeq1i  7306  djuexb  7337  djuf1olemr  7347  inresflem  7353  djuinr  7356  updjudhcoinlf  7373  updjudhcoinrg  7374  casefun  7378  caserel  7380  caseinj  7382  caseinl  7384  caseinr  7385  omp1eomlem  7387  endjusym  7389  difinfsn  7393  difinfinf  7394  djuinj  7399  0ct  7400  ctmlemr  7401  ctssdclemn0  7403  ctssdccl  7404  omct  7410  ctfoex  7411  finomni  7433  exmidomni  7435  fodjuomni  7442  ctssexmid  7443  fodjumkv  7453  nninfwlporlem  7466  nninfwlpoimlemg  7468  nninfwlpoim  7472  nninfinfwlpo  7473  card0  7486  ficardon  7487  exmidonfinlem  7498  dju1p1e2  7502  exmidfodomrlemim  7506  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  iftrueb01  7535  3nelsucpw1  7546  sucpw1nss3  7547  3nsssucpw1  7548  fmelpw1o  7559  2onetap  7571  exmidmotap  7577  0npi  7630  dmaddpi  7642  dmmulpi  7643  1lt2pi  7657  0nnq  7681  1nq  7683  dmaddpq  7696  dmmulpq  7697  rec1nq  7712  1lt2nq  7723  halfnqq  7727  prarloclemarch2  7736  enq0enq  7748  nqnq0pi  7755  nnnq0lem1  7763  addnnnq0  7766  mulnnnq0  7767  nq0m0r  7773  addpinq1  7781  prarloclem5  7817  prarloclemcalc  7819  1pr  7871  1idprl  7907  1idpru  7908  ltexprlemm  7917  recexprlem1ssl  7950  recexprlem1ssu  7951  suplocexprlemell  8030  suplocexprlem2b  8031  suplocexprlemmu  8035  suplocexprlemdisj  8037  suplocexprlemloc  8038  suplocexprlemub  8040  suplocexprlemlub  8041  prsrlem1  8059  addsrpr  8062  mulsrpr  8063  gt0srpr  8065  0nsr  8066  0r  8067  1sr  8068  m1r  8069  m1m1sr  8078  caucvgsr  8119  suplocsrlempr  8124  addresr  8154  mulresr  8155  pitonnlem1  8162  peano1nnnn  8169  axi2m1  8192  axcnre  8198  peano5nnnn  8209  axcaucvg  8217  mpomulf  8266  mulridi  8278  mullidi  8279  pnfnre  8317  mnfnre  8318  pnfnemnf  8330  mnfxr  8332  rexri  8333  ltnri  8368  ltleii  8378  00id  8416  addridi  8417  addlidi  8418  0cnALT  8465  negeqi  8469  negicn  8476  neg0  8521  renegcli  8537  negcli  8543  negidi  8544  negnegi  8545  subidi  8546  subid1i  8547  negne0bi  8548  negrebi  8549  mul02i  8665  mul01i  8666  mulm1i  8678  leidi  8761  gt0ne0ii  8763  inelr  8860  msqge0i  8893  gt0ap0ii  8904  1div1e1  8980  div1i  9016  eqnegi  9017  recclapi  9018  recidapi  9019  divmulapi  9042  rerecclapi  9053  redivclapi  9055  rerecapb  9119  recgt0  9126  ltp1i  9181  divgt0ii  9195  ltmul1ii  9204  ltdiv1ii  9205  sup3exmid  9233  peano5nni  9242  nnrei  9248  1nn  9250  nngt0i  9269  neg1ap0  9348  2timesi  9369  times2i  9370  2nn  9401  3nn  9402  4nn  9403  5nn  9404  6nn  9405  7nn  9406  8nn  9407  9nn  9408  2muline0  9465  rehalfcli  9489  nn0ssre  9502  nnnn0i  9506  dfn2  9511  0nn0  9513  nn0ge0i  9525  zrei  9585  neg1z  9611  nn0negzi  9614  dfz2  9652  nneoi  9685  peano5uzi  9690  dfuzi  9691  nn0ind-raph  9698  deceq1i  9718  deceq2i  9719  10nn  9727  numltc  9737  eluzel2  9861  eluz1i  9864  nn0uz  9892  nnuz  9893  uzuzle35  9900  infrenegsupex  9929  lbzbi  9951  divfnzn  9956  qdivcl  9978  irrmul  9982  irrmulap  9983  cnref1o  9986  0ltpnf  10118  mnflt0  10120  0lepnf  10126  xrltnsym  10129  xrlttri3  10133  nltpnft  10150  ngtmnft  10153  xrrebnd  10155  xnegmnf  10165  xneg0  10167  xltnegi  10171  xaddmnf1  10184  xaddmnf2  10185  mnfaddpnf  10187  xaddid1  10198  xnn0lenn0nn0  10201  xnn0xadd0  10203  xposdif  10218  ixxex  10235  iooval2  10251  unirnioo  10309  ioorebasg  10311  elrege0  10312  fzval2  10348  fzen  10380  fzprval  10420  fztpval  10421  uzdisj  10431  ige2m1fz  10448  fz01or  10449  fz1ssfz0  10455  fz0sn  10459  fz0tp  10460  fz0to3un2pr  10461  fz0to4untppr  10462  nn0disj  10476  1fv  10477  4fvwrd4  10478  fzo0ss1  10514  fzo01  10565  fzo12sn  10566  fzo0to2pr  10567  fzo0to3tp  10568  fzo0to42pr  10569  zsupssdc  10602  qbtwnxr  10621  flval  10636  fldiv4lem1div2  10671  modqfrac  10703  modqmulnn  10708  q2txmodxeq0  10750  frecuzrdgdom  10784  frecuzrdgfun  10786  frecuzrdgsuct  10790  frechashgf1o  10794  nnct  10801  xnn0nnen  10803  fxnn0nninf  10805  0tonninf  10806  1tonninf  10807  iseqvalcbv  10825  ser0f  10900  0exp0e1  10910  qexpcl  10921  qexpclz  10926  m1expcl2  10927  1exp  10934  sqvali  10985  sqcli  10986  sqeq0i  10987  resqcli  10990  sq1  10999  neg1sqe1  11000  iexpcyc  11010  qsqeqor  11016  facnn  11093  fac0  11094  fac1  11095  fac2  11097  fac3  11098  fac4  11099  bcval  11115  bcm1k  11126  bcpasc  11132  bccl  11133  4bc3eq4  11140  4bc2eq6  11141  hashinfom  11145  hashennn  11147  hashfz1  11150  fihasheq0  11160  hash0  11163  hashsng  11165  fihashen1  11166  en1hash  11167  omgadd  11170  hashp1i  11179  hashxp  11195  hashpwfi  11197  fimaxq  11198  ssenneg  11208  hashfibc  11211  zfz1iso  11217  hash2en  11219  wrdexi  11241  wrdv  11244  wrdeqi  11251  wrd0  11253  lsw0  11276  ccatclab  11286  ccatidid  11302  s1prc  11315  ccat1st1st  11333  swrds1  11364  fnpfx  11373  swrdccatin2  11425  pfxccatin12lem2  11427  cats1fvn  11460  shftidt2  11521  cjexp  11582  re0  11584  im0  11585  re1  11586  im1  11587  cj0  11590  cji  11591  recli  11600  imcli  11601  cjcli  11602  replimi  11603  cjcji  11604  reim0bi  11605  rerebi  11606  cjrebi  11607  recji  11608  imcji  11609  cjmulrcli  11610  cjmulvali  11611  cjmulge0i  11612  renegi  11613  imnegi  11614  cjnegi  11615  addcji  11616  uzin2  11676  rexanuz  11677  rexfiuz  11678  sqrtrval  11689  sqrt0  11693  resqrexlemcalc3  11705  resqrexlemcvg  11708  resqrex  11715  abs0  11747  absi  11748  qabsor  11764  absimle  11773  recan  11798  caubnd2  11806  leabsi  11817  absrei  11818  sqrtpclii  11819  sqrtgt0ii  11820  absvalsqi  11829  absvalsq2i  11830  abscli  11831  absge0i  11832  absval2i  11833  abs00i  11834  absgt0api  11835  absnegi  11836  abscji  11837  releabsi  11838  infxrnegsupex  11952  xrbdtri  11965  cbvsum  12049  sumeq1i  12052  sum0  12078  isumz  12079  fisumss  12082  fsumsersdc  12085  fsumadd  12096  isumclim  12111  isumclim3  12113  fsumcnv  12127  modfsummodlem1  12146  fsumrelem  12161  binomlem  12173  binom  12174  arisum2  12189  expcnv  12194  0.999...  12211  prodf1f  12233  cbvprod  12248  prodeq1i  12251  zproddc  12269  zprodap0  12271  prod0  12275  fprodssdc  12280  prodsnf  12282  fprodcnv  12315  fprodge0  12327  fprodge1  12329  ef0lem  12350  esum  12352  ere  12360  ege2le3  12361  ef0  12362  eff2  12370  efsep  12381  reeff1  12390  sin0  12419  cos0  12420  ef01bndlem  12446  cos2bnd  12450  sincos1sgn  12455  sincos2sgn  12456  sin4lt0  12457  eirr  12469  0dvds  12501  dvds1  12543  z0even  12601  n2dvdsm1  12603  z2even  12604  n2dvds3  12605  ndvdssub  12620  ndvdsi  12623  flodddiv4  12626  bits0  12638  bitsfzo  12645  0bits  12649  m1bits  12650  bitsinv1lem  12651  bitsinv1  12652  gcddvds  12663  gcd1  12687  6gcd4e2  12695  bezoutlembi  12705  dfgcd3  12710  dfgcd2  12714  nninfctlemfo  12740  nninfct  12741  3lcm2e6woprm  12787  qredeu  12798  isprm2lem  12817  isprm3  12819  prm2orodd  12827  isprm5lem  12842  sqrt2irr0  12865  pw2dvds  12867  phicl2  12915  phi1  12920  dfphi2  12921  phiprmpw  12923  eulerthlemrprm  12930  eulerthlemh  12932  odzval  12943  oddprm  12961  pczpre  12999  pcdiv  13004  pc0  13006  pcqdiv  13009  pcrec  13010  pcexp  13011  pcxcl  13013  pcxqcl  13014  pcdvdstr  13029  pc2dvds  13032  dvdsprmpweqnn  13038  pcmpt  13045  qexpz  13054  pockthi  13060  1arith2  13070  4sqlemffi  13098  4sqlem11  13103  4sqlem13m  13105  4sqlem19  13111  dec2dvds  13113  dec5nprm  13116  modxai  13118  modxp1i  13120  numexp0  13124  numexp1  13125  ballotfilem1  13143  ballotfilemonn  13144  ballotfilem2  13149  ballotfilemfc0  13153  ballotfilemfcc  13154  ballotfilem4  13159  ennnfonelemp1  13174  ennnfonelem1  13175  ennnfonelemkh  13180  ennnfonelemex  13182  ennnfonelemnn0  13190  ennnfonelemr  13191  exmidunben  13194  ctinfomlemom  13195  ctinfom  13196  ctinf  13198  qnnen  13199  omctfn  13211  omiunct  13212  ssnnctlemct  13214  nninfdc  13221  structcnvcnv  13245  structfun  13247  structfn  13248  ndxarg  13252  ndxid  13253  setsresg  13267  setsslnid  13281  basmex  13289  basmexd  13290  strleun  13334  strle1g  13336  prdsex  13499  prdsvallem  13502  prdsval  13503  prdsbaslemss  13504  imasaddfnlemg  13544  quslem  13554  xpsfrnel  13574  xpsff1o  13579  ismgmn0  13588  fn0g  13605  0g0  13606  fngsum  13618  idghm  13993  rhmfn  14334  rmodislmodlem  14515  rmodislmod  14516  lidlmex  14640  mopnset  14717  cntopex  14719  cnfldex  14724  cnfldbas  14725  mpocnfldadd  14726  mpocnfldmul  14728  cnfldcj  14730  cnfldtset  14731  cnfldle  14732  cnfldds  14733  cnring  14735  cnfld0  14736  cnfld1  14737  cnfldneg  14738  cnfldplusf  14739  cnfldsub  14740  cnfldmulg  14741  cnfldexp  14742  cnsubglem  14744  cnsubrglem  14745  gzsubrg  14747  gsumfzfsumlem0  14751  cnfldui  14754  zringring  14758  zringabl  14759  zringgrp  14760  zring1  14766  zringsubgval  14770  expghmap  14772  znval  14801  znle  14802  znbaslemnn  14804  znbas  14809  znzrh2  14811  znzrhval  14812  znzrhfo  14813  znleval  14818  znidom  14822  znidomb  14823  fnpsr  14832  psrelbas  14847  psradd  14851  psraddcl  14852  psr1clfi  14860  mplrcl  14866  mplbasss  14868  mpladd  14876  istopon  14895  topontopi  14898  toponunii  14899  toponrestid  14903  istps  14914  topontopn  14919  eltpsi  14923  eltg4i  14937  eltg3  14939  tg1  14941  tg2  14942  tgclb  14947  topnex  14968  sn0topon  14970  distps  14973  cldrcl  14984  sn0cld  15019  restco  15056  lmrcl  15074  ssidcn  15092  cnconst2  15115  cnptopresti  15120  cnptoprest  15121  txuni2  15138  txbas  15140  eltx  15141  txcnp  15153  upxp  15154  txcnmpt  15155  uptx  15156  txcn  15157  txrest  15158  txlm  15161  cnmptid  15163  cnmpt1st  15170  cnmpt2nd  15171  hmeofn  15184  psmetge0  15213  ismeti  15228  xmetunirn  15240  xmetge0  15247  unirnblps  15304  unirnbl  15305  mopnex  15387  qtopbasss  15403  retop  15406  uniretop  15407  iooretopg  15410  cnxmet  15413  cntoptopon  15414  cnbl0  15416  cnfldxms  15419  cnfldtps  15420  rexmet  15431  blssioo  15435  tgioo  15436  tgqioo  15437  cnopnap  15493  hovercncf  15528  limcresi  15548  dvfvalap  15563  dvidlemap  15573  dvidrelem  15574  dvidsslem  15575  dvcnp2cntop  15581  dvcoapbr  15589  dvexp2  15594  dvrecap  15595  dveflem  15608  dvef  15609  plyun0  15618  plyrecj  15645  dvply2  15649  reeff1o  15655  sin0pilem1  15663  sin0pilem2  15664  pilem3  15665  pigt2lt4  15666  pire  15668  sinhalfpilem  15673  pidiv2halves  15677  cosneghalfpi  15680  cospi  15682  efipi  15683  sin2pi  15685  cos2pi  15686  ef2pi  15687  cosq14gt0  15714  coseq00topi  15717  coseq0negpitopi  15718  sincos4thpi  15722  sincos6thpi  15724  sincos3rdpi  15725  pigt3  15726  cos02pilt1  15733  ioocosf1o  15736  dfrelog  15742  relogf1o  15743  relogcl  15744  relogiso  15755  rpcxpsqrt  15804  rpabscxpbnd  15822  2logb9irr  15853  2logb9irrALT  15856  sqrt2cxp2logb9e3  15857  2irrexpq  15858  2logb9irrap  15859  2irrexpqap  15860  mpodvdsmulf1o  15875  fsumdvdsmul  15876  perfectlem2  15885  lgsdir2lem1  15918  lgsdir2lem2  15919  lgsdir2lem4  15921  lgsdir2lem5  15922  lgsdi  15927  gausslemma2dlem0i  15947  gausslemma2dlem4  15954  lgseisenlem4  15963  lgsquadlem1  15967  lgsquad2lem2  15972  lgsquad2  15973  m1lgs  15975  2lgs2  15992  2lgslem4  15993  2lgsoddprmlem2  15996  2lgsoddprmlem3c  15999  2lgsoddprmlem3d  16000  2sqlem9  16014  2sqlem10  16015  1vgrex  16032  vtxval0  16065  iedgval0  16066  uhgr0  16097  upgrfi  16114  umgrislfupgrdom  16143  ausgrusgrben  16180  uspgredgiedg  16190  uspgriedgedg  16191  usgrislfuspgrdom  16202  uspgredg2vlem  16232  uspgredg2v  16233  usgr0  16251  griedg0prc  16262  subupgr  16285  vdegp1cid  16328  0wlk0  16383  clwwlkn1  16430  clwwlkn2  16433  eupth2lem1  16470  eulerpathum  16493  konigsbergiedgwen  16496  konigsberglem1  16500  konigsberglem3  16502  konigsberglem4  16503  konigsberglem5  16504  konigsberg  16505  ex-fl  16510  ex-ceil  16511  ex-exp  16512  ex-fac  16513  ex-gcd  16516  bj-stfal  16531  bj-stst  16534  bj-dcfal  16544  bj-dcdc  16548  bj-stdc  16549  bj-dcst  16550  bj-el2oss1o  16563  elabf2  16571  bd0  16611  bdeli  16633  bdcriota  16670  bdbm1.3ii  16678  bdinex1  16686  bdssexi  16690  bj-inex  16694  bj-snex  16700  bj-sucex  16710  bj-d0clsepcl  16712  bj-omind  16721  bj-om  16724  bj-2inf  16725  bj-peano2  16726  bdpeano5  16730  bj-omssonALT  16750  bj-inf2vnlem1  16757  bj-omex2  16764  bj-nn0sucALT  16765  3dom  16779  012of  16784  2o01f  16785  subctctexmid  16791  pw1dceq  16795  exmidpeirce  16798  nninfall  16804  nninfsellemqall  16810  nninfsellemeqinf  16811  nninfomnilem  16813  nninfomni  16814  exmidsbthrlem  16819  sbthom  16823  isomninnlem  16831  isomninn  16832  cvgcmp2nlemabs  16833  iooreen  16836  trilpolemisumle  16839  trilpolemeq1  16841  trilpo  16844  trirec0  16845  apdifflemr  16848  qdiff  16850  iswomninnlem  16851  iswomninn  16852  ismkvnnlem  16854  ismkvnn  16855  redcwlpo  16857  dcapnconst  16864  nconstwlpolem0  16866  nconstwlpo  16869  neapmkv  16871  neap0mkv  16872  taupi  16876  gfsumsn  16884  gfsumcl  16887