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 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  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  3702  pwid  3706  sneqi  3720  elsn  3724  elpr  3729  elsn2  3742  ralsn  3751  rexsn  3752  eltp  3756  rabrsndc  3778  preq1i  3790  preq2i  3791  prid1  3816  snnz  3830  snm  3831  prnz  3834  prm  3835  tpnz  3837  snss  3848  snsssn  3884  opeq1i  3905  opeq2i  3906  unieqi  3943  unissi  3956  inteqi  3972  intmin2  3994  intab  3997  intsn  4003  iinconstm  4019  iuniin  4020  iinss1  4022  iunxdif2  4059  ssiinf  4060  iinss  4062  iinss2  4063  iinab  4072  iundif2ss  4076  iindif2m  4078  iinin2m  4079  iunxsn  4087  iunxprg  4091  iinpw  4101  invdisjrab  4122  sndisj  4124  disjxsn  4126  breqi  4134  breq1i  4135  breq2i  4136  brab1  4176  opabbii  4196  truni  4241  sepgi  4250  bm1.3ii  4252  a9evsep  4253  ax9vsep  4254  zfnuleu  4255  axnul  4256  ssexi  4269  difexi  4274  rabex  4278  rabex2  4280  elpw2  4291  pwnss  4294  iin0r  4304  intv  4305  pwex  4318  snex  4320  notnotsnex  4322  ord3ex  4325  dtruarb  4326  undifexmid  4328  intid  4362  opnzi  4373  copsexg  4382  opwo0id  4387  opelopabf  4415  epelc  4434  elon  4517  inton  4536  onn0  4543  onm  4544  elsuc  4549  elsuc2  4550  sucid  4560  iunsuc  4563  onordi  4569  ontrci  4570  onelssi  4572  eusvnf  4597  ssonunii  4634  sucex  4644  onssi  4660  onsuci  4661  ordtriexmidlem  4664  ordtriexmidlem2  4665  ordtriexmid  4666  ontriexmidim  4667  ordtri2orexmid  4668  2ordpr  4669  ontr2exmid  4670  onsucsssucexmid  4672  onsucelsucexmid  4675  regexmidlemm  4677  reg2exmid  4681  onirri  4688  ruALT  4696  onprc  4697  sucon  4698  dtru  4705  0elsucexmid  4710  ordpwsucexmid  4715  ordtri2or2exmid  4716  ontri2orexmidim  4717  dcextest  4726  omex  4738  find  4744  omelon  4754  nnoni  4756  limom  4759  nnregexmid  4766  omsinds  4767  xpeq1i  4792  xpeq2i  4793  0nelxp  4800  opthprc  4824  mosubop  4839  releqi  4856  relssi  4864  relin1  4893  relin2  4894  reldif  4895  inopab  4910  difopab  4911  xpiindim  4915  opabbi2dv  4927  ideq  4930  coeq1i  4937  coeq2i  4938  cnveqi  4953  eldm  4976  eldm2  4977  dmeqi  4980  dmv  4995  rneqi  5008  elrnmpti  5033  dmex  5047  rnex  5048  reseq1i  5057  reseq2i  5058  residm  5093  resex  5102  resmpt3  5110  imaeq1i  5121  imaeq2i  5122  elima  5129  imaex  5139  elimasn  5152  args  5154  epini  5156  dfse2  5158  eliniseg2  5165  relbrcnv  5166  cotr  5167  issref  5168  cnvsym  5169  asymref  5171  intirr  5172  codir  5174  qfto  5175  ssrnres  5228  cnveq0  5242  cnvsn0  5254  dmsnop  5259  rnsnop  5266  resdm2  5276  dfco2a  5286  cocnvcnv1  5296  coi2  5302  coires1  5303  cnvssrndm  5307  cossxp  5308  cocnvres  5310  relrelss  5312  relcoi2  5316  unidmrn  5318  dfdm2  5320  unixpm  5321  cnvexg  5323  cnvex  5324  cnviinm  5327  iotaval  5347  funeqi  5396  funi  5407  funres  5416  funcnvsn  5424  funcnvcnv  5438  funin  5450  funcnvres  5452  isarep2  5466  fneq1i  5473  fneq2i  5474  fndmi  5479  fnresdisj  5491  fnresi  5499  mpt0  5509  dmmpti  5511  feq1i  5524  feq2i  5525  fdmi  5539  fun2  5560  fssres  5563  resasplitss  5567  fintm  5575  fconst6  5590  f1ores  5652  foimacnv  5655  resdif  5659  funcocnv2  5662  f10d  5673  f1ovi  5678  fveq1i  5694  fveq2i  5696  0fv  5731  fvun1  5766  fvopab3ig  5776  fvmptss2  5777  mptrcl  5785  elfvmptrab1  5797  fndmdif  5808  fneqeql2  5812  f1oresrab  5867  fmptco  5868  funopsn  5885  fnressn  5895  fressnfv  5896  fmptap  5899  fvsnun1  5906  fvsnun2  5907  fsnunfv  5910  fconst2  5926  mptex  5937  fnfvimad  5947  rinvf1o  6028  riotabiia  6050  acexmidlema  6069  acexmidlemb  6070  acexmidlemcase  6073  acexmidlem2  6075  acexmidlemv  6076  oveq1i  6088  oveq2i  6089  oveqi  6091  oprabidlem  6109  0neqopab  6126  oprabbii  6136  oprabss  6167  mpompt  6173  funoprab  6181  fnoprab  6184  ovigg  6202  elmpocl  6277  relmptopab  6284  resfunexgALT  6330  cofunexg  6331  mptexw  6335  opabex3d  6343  opabex3  6344  1st0  6371  2nd0  6372  op1st  6373  op2nd  6374  f1stres  6386  f2ndres  6387  fo1stresm  6388  fo2ndresm  6389  1stcof  6390  2ndcof  6391  1stexg  6394  2ndexg  6395  releldm2  6412  reldm  6413  dfoprab3  6418  mpomptsx  6426  mpompts  6427  fnmpoi  6432  dmmpo  6433  mpoexxg  6439  mpoexw  6442  1stconst  6450  2ndconst  6451  dfmpo  6452  algrflem  6458  algrflemg  6459  cnvoprab  6463  f1od2  6464  elmpom  6467  mpoxopn0yelv  6503  mpoxopoveq  6504  tposssxp  6513  brtpos2  6515  reldmtpos  6517  dftpos2  6525  dftpos4  6527  tpostpos  6528  tpostpos2  6529  tposfo  6535  tposf  6536  tposeqi  6541  tposex  6542  tposoprab  6544  issmo  6552  smores  6556  smores2  6558  iordsmo  6561  smo0  6562  tfrlem8  6582  tfrexlem  6598  tfr1onlem3  6602  tfr1onlemsucaccv  6605  tfr1onlembxssdm  6607  tfr1onlemres  6613  tfri1dALT  6615  tfri2  6630  rdgisuc1  6648  rdg0  6651  frecfun  6659  frec0g  6661  freccllem  6666  frecfcllem  6668  frecsuclem  6670  frecrdg  6672  2on0  6690  xp01disj  6699  2oconcl  6705  fnoa  6713  oaexg  6714  fnom  6716  omexg  6717  fnoei  6718  oeiexg  6719  oei0  6725  oacl  6726  oasuc  6730  o1p1e2  6734  omsuc  6738  nna0r  6744  nnm0r  6745  1onn  6786  2onn  6787  3onn  6788  4onn  6789  2ssom  6790  eqerlem  6831  eceq2i  6838  elqs  6853  qsex  6859  ecqs  6864  iinerm  6874  th3qlem1  6904  th3q  6907  mapsn  6965  mapsnf1o3  6972  ixpiinm  6999  ixpssmap  7007  brdom  7027  f1dom  7039  enref  7044  dom2  7054  idssen  7056  ssdomg  7058  ensymi  7062  ensn1  7076  fiprc  7097  1domsn  7108  dom1o  7109  xpcomf1o  7116  xpcomco  7117  dom0  7131  0dom  7132  xpmapenlem  7142  phplem2  7147  php5  7152  snnen2og  7153  1nen2  7155  php5dom  7157  ssfilem  7170  ssfiexmid  7171  ssfilemd  7172  ssfiexmidt  7173  domfiexmid  7175  0fi  7181  diffitest  7184  findcard  7185  findcard2  7186  findcard2s  7187  isinfinf  7194  ac6sfi  7195  inffiexmid  7206  pw1fin  7210  unfiexmid  7218  xpfi  7232  fisseneq  7235  ssfirab  7237  residfi  7247  mapfi  7254  en1eqsn  7258  snexxph  7260  sbthlem2  7268  sbthlemi3  7269  sbthlemi6  7272  sbthlem7  7273  fi0  7302  fipwfi  7314  supeq1i  7321  infeq1i  7346  djuexb  7377  djuf1olemr  7387  inresflem  7393  djuinr  7396  updjudhcoinlf  7413  updjudhcoinrg  7414  casefun  7418  caserel  7420  caseinj  7422  caseinl  7424  caseinr  7425  omp1eomlem  7427  endjusym  7429  difinfsn  7433  difinfinf  7434  djuinj  7439  0ct  7440  ctmlemr  7441  ctssdclemn0  7443  ctssdccl  7444  omct  7450  ctfoex  7451  finomni  7473  exmidomni  7475  fodjuomni  7482  ctssexmid  7483  fodjumkv  7493  nninfwlporlem  7506  nninfwlpoimlemg  7508  nninfwlpoim  7512  nninfinfwlpo  7513  card0  7526  ficardon  7527  exmidonfinlem  7538  dju1p1e2  7542  exmidfodomrlemim  7546  exmidfodomrlemr  7547  exmidfodomrlemrALT  7548  iftrueb01  7575  3nelsucpw1  7586  sucpw1nss3  7587  3nsssucpw1  7588  fmelpw1o  7599  2onetap  7614  exmidmotap  7620  0npi  7673  dmaddpi  7685  dmmulpi  7686  1lt2pi  7700  0nnq  7724  1nq  7726  dmaddpq  7739  dmmulpq  7740  rec1nq  7755  1lt2nq  7766  halfnqq  7770  prarloclemarch2  7779  enq0enq  7791  nqnq0pi  7798  nnnq0lem1  7806  addnnnq0  7809  mulnnnq0  7810  nq0m0r  7816  addpinq1  7824  prarloclem5  7860  prarloclemcalc  7862  1pr  7914  1idprl  7950  1idpru  7951  ltexprlemm  7960  recexprlem1ssl  7993  recexprlem1ssu  7994  suplocexprlemell  8073  suplocexprlem2b  8074  suplocexprlemmu  8078  suplocexprlemdisj  8080  suplocexprlemloc  8081  suplocexprlemub  8083  suplocexprlemlub  8084  prsrlem1  8102  addsrpr  8105  mulsrpr  8106  gt0srpr  8108  0nsr  8109  0r  8110  1sr  8111  m1r  8112  m1m1sr  8121  caucvgsr  8162  suplocsrlempr  8167  addresr  8197  mulresr  8198  pitonnlem1  8205  peano1nnnn  8212  axi2m1  8235  axcnre  8241  peano5nnnn  8252  axcaucvg  8260  mpomulf  8309  mulridi  8321  mullidi  8322  pnfnre  8360  mnfnre  8361  pnfnemnf  8373  mnfxr  8375  rexri  8376  ltnri  8411  ltleii  8421  00id  8460  addridi  8461  addlidi  8462  0cnALT  8509  negeqi  8513  negicn  8520  neg0  8565  renegcli  8581  negcli  8587  negidi  8588  negnegi  8589  subidi  8590  subid1i  8591  negne0bi  8592  negrebi  8593  mul02i  8710  mul01i  8711  mulm1i  8723  leidi  8806  gt0ne0ii  8808  inelr  8905  msqge0i  8938  gt0ap0ii  8949  1div1e1  9027  div1i  9063  eqnegi  9064  recclapi  9065  recidapi  9066  divmulapi  9089  rerecclapi  9100  redivclapi  9102  rerecapb  9166  recgt0  9173  ltp1i  9228  divgt0ii  9242  ltmul1ii  9251  ltdiv1ii  9252  sup3exmid  9280  peano5nni  9289  nnrei  9295  1nn  9297  nngt0i  9316  neg1ap0  9395  2timesi  9416  times2i  9417  2nn  9448  3nn  9449  4nn  9450  5nn  9451  6nn  9452  7nn  9453  8nn  9454  9nn  9455  2muline0  9512  rehalfcli  9536  nn0ssre  9549  nnnn0i  9553  dfn2  9558  0nn0  9560  nn0ge0i  9572  zrei  9632  neg1z  9658  nn0negzi  9661  dfz2  9699  nneoi  9732  peano5uzi  9737  dfuzi  9738  nn0ind-raph  9745  deceq1i  9765  deceq2i  9766  10nn  9774  numltc  9784  eluzel2  9908  eluz1i  9911  nn0uz  9939  nnuz  9940  uzuzle35  9947  infrenegsupex  9976  lbzbi  9998  divfnzn  10003  qdivcl  10025  irrmul  10029  irrmulap  10030  cnref1o  10033  0ltpnf  10166  mnflt0  10168  0lepnf  10174  xrltnsym  10177  xrlttri3  10181  nltpnft  10198  ngtmnft  10201  xrrebnd  10203  xnegmnf  10213  xneg0  10215  xltnegi  10219  xaddmnf1  10232  xaddmnf2  10233  mnfaddpnf  10235  xaddid1  10246  xnn0lenn0nn0  10249  xnn0xadd0  10251  xposdif  10266  ixxex  10283  iooval2  10299  unirnioo  10357  ioorebasg  10359  elrege0  10360  fzval2  10396  fzen  10429  fzprval  10470  fztpval  10471  uzdisj  10481  ige2m1fz  10498  fz01or  10499  fz1ssfz0  10505  fz0sn  10509  fz0tp  10510  fz0to3un2pr  10511  fz0to4untppr  10512  nn0disj  10526  1fv  10527  4fvwrd4  10528  fzo0ss1  10564  fzo01  10615  fzo12sn  10616  fzo0to2pr  10617  fzo0to3tp  10618  fzo0to42pr  10619  zsupssdc  10654  qbtwnxr  10673  flval  10688  fldiv4lem1div2  10723  modqfrac  10755  modqmulnn  10760  q2txmodxeq0  10802  frecuzrdgdom  10836  frecuzrdgfun  10838  frecuzrdgsuct  10842  frechashgf1o  10846  nnct  10853  xnn0nnen  10855  fxnn0nninf  10857  0tonninf  10858  1tonninf  10859  iseqvalcbv  10877  ser0f  10952  0exp0e1  10962  qexpcl  10973  qexpclz  10978  m1expcl2  10979  1exp  10986  sqvali  11037  sqcli  11038  sqeq0i  11039  resqcli  11042  sq1  11051  neg1sqe1  11052  iexpcyc  11062  qsqeqor  11068  facnn  11146  fac0  11147  fac1  11148  fac2  11150  fac3  11151  fac4  11152  bcval  11168  bcm1k  11179  bcpasc  11185  bccl  11186  4bc3eq4  11193  4bc2eq6  11194  hashinfom  11198  hashennn  11200  hashfz1  11203  fihasheq0  11213  hash0  11216  hashsng  11218  fihashen1  11219  en1hash  11220  omgadd  11223  hashp1i  11232  hashxp  11248  hashpwfi  11250  fimaxq  11251  ssenneg  11261  hashfibc  11264  hashf1lem1  11266  hashf1  11268  zfz1iso  11274  hash2en  11276  wrdexi  11298  wrdv  11301  wrdeqi  11308  wrd0  11310  lsw0  11333  ccatclab  11343  ccatidid  11359  s1prc  11372  ccat1st1st  11390  swrds1  11421  fnpfx  11430  swrdccatin2  11482  pfxccatin12lem2  11484  cats1fvn  11517  shftidt2  11578  cjexp  11639  re0  11642  im0  11643  re1  11644  im1  11645  cj0  11648  cji  11649  recli  11658  imcli  11659  cjcli  11660  replimi  11661  cjcji  11662  reim0bi  11663  rerebi  11664  cjrebi  11665  recji  11666  imcji  11667  cjmulrcli  11668  cjmulvali  11669  cjmulge0i  11670  renegi  11671  imnegi  11672  cjnegi  11673  addcji  11674  uzin2  11734  rexanuz  11735  rexfiuz  11736  sqrtrval  11747  sqrt0  11751  resqrexlemcalc3  11763  resqrexlemcvg  11766  resqrex  11773  abs0  11805  absi  11806  qabsor  11822  absimle  11831  recan  11856  caubnd2  11864  leabsi  11875  absrei  11876  sqrtpclii  11877  sqrtgt0ii  11878  absvalsqi  11887  absvalsq2i  11888  abscli  11889  absge0i  11890  absval2i  11891  abs00i  11892  absgt0api  11893  absnegi  11894  abscji  11895  releabsi  11896  infxrnegsupex  12010  xrbdtri  12023  cbvsum  12107  sumeq1i  12110  sum0  12136  isumz  12137  fisumss  12140  fsumsersdc  12143  fsumadd  12154  isumclim  12169  isumclim3  12171  fsumcnv  12185  modfsummodlem1  12204  fsumrelem  12219  binomlem  12231  binom  12232  arisum2  12247  expcnv  12252  0.999...  12269  prodf1f  12291  cbvprod  12306  prodeq1i  12309  zproddc  12327  zprodap0  12329  prod0  12333  fprodssdc  12338  prodsnf  12340  fprodcnv  12373  fprodge0  12385  fprodge1  12387  ef0lem  12408  esum  12410  ere  12418  ege2le3  12419  ef0  12420  eff2  12428  efsep  12439  reeff1  12448  sin0  12477  cos0  12478  ef01bndlem  12504  cos2bnd  12508  sincos1sgn  12513  sincos2sgn  12514  sin4lt0  12515  eirr  12527  0dvds  12559  dvds1  12601  z0even  12659  n2dvdsm1  12661  z2even  12662  n2dvds3  12663  ndvdssub  12678  ndvdsi  12681  flodddiv4  12684  bits0  12696  bitsfzo  12703  0bits  12707  m1bits  12708  bitsinv1lem  12709  bitsinv1  12710  gcddvds  12721  gcd1  12745  6gcd4e2  12753  bezoutlembi  12763  dfgcd3  12768  dfgcd2  12772  nninfctlemfo  12798  nninfct  12799  3lcm2e6woprm  12845  qredeu  12856  isprm2lem  12875  isprm3  12877  prm2orodd  12885  isprm5lem  12900  sqrt2irr0  12923  pw2dvds  12925  phicl2  12973  phi1  12978  dfphi2  12979  phiprmpw  12981  eulerthlemrprm  12988  eulerthlemh  12990  odzval  13001  oddprm  13019  pczpre  13057  pcdiv  13062  pc0  13064  pcqdiv  13067  pcrec  13068  pcexp  13069  pcxcl  13071  pcxqcl  13072  pcdvdstr  13087  pc2dvds  13090  dvdsprmpweqnn  13096  pcmpt  13103  qexpz  13112  pockthi  13118  1arith2  13128  4sqlemffi  13156  4sqlem11  13161  4sqlem13m  13163  4sqlem19  13169  dec2dvds  13171  dec5nprm  13174  modxai  13176  modxp1i  13178  numexp0  13182  numexp1  13183  ballotfilem1  13201  ballotfilemonn  13202  ballotfilem2  13209  ballotfilemfc0  13213  ballotfilemfcc  13214  ballotfilem4  13222  ballotfilemi  13224  ballotfilem7  13260  ballotfilem8  13261  ballotfilemth  13262  ennnfonelemp1  13278  ennnfonelem1  13279  ennnfonelemkh  13284  ennnfonelemex  13286  ennnfonelemnn0  13294  ennnfonelemr  13295  exmidunben  13298  ctinfomlemom  13299  ctinfom  13300  ctinf  13302  qnnen  13303  omctfn  13315  omiunct  13316  ssnnctlemct  13318  nninfdc  13325  structcnvcnv  13349  structfun  13351  structfn  13352  ndxarg  13356  ndxid  13357  setsresg  13371  setsslnid  13385  basmex  13393  basmexd  13394  strleun  13438  strle1g  13440  prdsvallem  13601  imasaddfnlemg  13615  quslem  13625  xpsfrnel  13645  xpsff1o  13650  ismgmn0  13658  fn0g  13675  0g0  13676  fngzsum  13688  idghm  14042  gsumsncmn  14136  gsumclfi  14139  gsummptfidmadd  14141  gsumsubmclfi  14143  gsumconstcmn  14146  prdsex  14152  prdsval  14153  prdsbaslemss  14154  rhmfn  14455  rmodislmodlem  14662  rmodislmod  14663  lidlmex  14787  mopnset  14864  cntopex  14866  cnfldex  14871  cnfldbas  14872  mpocnfldadd  14873  mpocnfldmul  14875  cnfldcj  14877  cnfldtset  14878  cnfldle  14879  cnfldds  14880  cnring  14882  cnfld0  14883  cnfld1  14884  cnfldneg  14885  cnfldplusf  14886  cnfldsub  14887  cnfldmulg  14888  cnfldexp  14889  cnsubglem  14891  cnsubrglem  14892  gzsubrg  14894  gsumfsum  14898  cnfldui  14899  zringring  14903  zringabl  14904  zringgrp  14905  zring1  14911  zringsubgval  14915  expghmap  14917  znval  14946  znle  14947  znbaslemnn  14949  znbas  14954  znzrh2  14956  znzrhval  14957  znzrhfo  14958  znleval  14963  znidom  14967  znidomb  14968  fnpsr  14977  psrelbas  14992  psradd  14996  psraddcl  14997  psr1clfi  15005  mplrcl  15011  mplbasss  15013  mpladd  15021  istopon  15040  topontopi  15043  toponunii  15044  toponrestid  15048  istps  15059  topontopn  15064  eltpsi  15068  eltg4i  15082  eltg3  15084  tg1  15086  tg2  15087  tgclb  15092  topnex  15113  sn0topon  15115  distps  15118  cldrcl  15129  sn0cld  15164  restco  15201  lmrcl  15219  ssidcn  15237  cnconst2  15260  cnptopresti  15265  cnptoprest  15266  txuni2  15283  txbas  15285  eltx  15286  txcnp  15298  upxp  15299  txcnmpt  15300  uptx  15301  txcn  15302  txrest  15303  txlm  15306  cnmptid  15308  cnmpt1st  15315  cnmpt2nd  15316  hmeofn  15329  psmetge0  15358  ismeti  15373  xmetunirn  15385  xmetge0  15392  unirnblps  15449  unirnbl  15450  mopnex  15532  qtopbasss  15548  retop  15551  uniretop  15552  iooretopg  15555  cnxmet  15558  cntoptopon  15559  cnbl0  15561  cnfldxms  15564  cnfldtps  15565  rexmet  15576  blssioo  15580  tgioo  15581  tgqioo  15582  cnopnap  15638  hovercncf  15673  limcresi  15693  dvfvalap  15708  dvidlemap  15718  dvidrelem  15719  dvidsslem  15720  dvcnp2cntop  15726  dvcoapbr  15734  dvexp2  15739  dvrecap  15740  dveflem  15753  dvef  15754  plyun0  15763  plyrecj  15790  dvply2  15794  reeff1o  15800  sin0pilem1  15808  sin0pilem2  15809  pilem3  15810  pigt2lt4  15811  pire  15813  sinhalfpilem  15818  pidiv2halves  15822  cosneghalfpi  15825  cospi  15827  efipi  15828  sin2pi  15830  cos2pi  15831  ef2pi  15832  cosq14gt0  15859  coseq00topi  15862  coseq0negpitopi  15863  sincos4thpi  15867  sincos6thpi  15869  sincos3rdpi  15870  pigt3  15871  cos02pilt1  15878  ioocosf1o  15881  dfrelog  15887  relogf1o  15888  relogcl  15889  relogiso  15900  logfac  15921  rpcxpsqrt  15950  rpabscxpbnd  15968  2logb9irr  15999  2logb9irrALT  16002  sqrt2cxp2logb9e3  16003  2irrexpq  16004  2logb9irrap  16005  2irrexpqap  16006  mpodvdsmulf1o  16021  fsumdvdsmul  16022  perfectlem2  16031  lgsdir2lem1  16064  lgsdir2lem2  16065  lgsdir2lem4  16067  lgsdir2lem5  16068  lgsdi  16073  gausslemma2dlem0i  16093  gausslemma2dlem4  16100  lgseisenlem4  16109  lgsquadlem1  16113  lgsquad2lem2  16118  lgsquad2  16119  m1lgs  16121  2lgs2  16138  2lgslem4  16139  2lgsoddprmlem2  16142  2lgsoddprmlem3c  16145  2lgsoddprmlem3d  16146  2sqlem9  16160  2sqlem10  16161  1vgrex  16178  vtxval0  16211  iedgval0  16212  uhgr0  16243  upgrfi  16260  umgrislfupgrdom  16289  ausgrusgrben  16326  uspgredgiedg  16336  uspgriedgedg  16337  usgrislfuspgrdom  16348  uspgredg2vlem  16378  uspgredg2v  16379  usgr0  16397  griedg0prc  16408  subupgr  16431  vdegp1cid  16474  0wlk0  16529  clwwlkn1  16576  clwwlkn2  16579  eupth2lem1  16616  eulerpathum  16639  konigsbergiedgwen  16642  konigsberglem1  16646  konigsberglem3  16648  konigsberglem4  16649  konigsberglem5  16650  konigsberg  16651  ex-fl  16656  ex-ceil  16657  ex-exp  16658  ex-fac  16659  ex-gcd  16662  bj-stfal  16687  bj-stst  16690  bj-dcfal  16700  bj-dcdc  16704  bj-stdc  16705  bj-dcst  16706  bj-el2oss1o  16719  elabf2  16727  bd0  16767  bdeli  16789  bdcriota  16826  bdbm1.3ii  16834  bdinex1  16842  bdssexi  16846  bj-inex  16850  bj-snex  16856  bj-sucex  16866  bj-d0clsepcl  16868  bj-omind  16877  bj-om  16880  bj-2inf  16881  bj-peano2  16882  bdpeano5  16886  bj-omssonALT  16906  bj-inf2vnlem1  16913  bj-omex2  16920  bj-nn0sucALT  16921  3dom  16935  012of  16940  2o01f  16941  subctctexmid  16947  pw1dceq  16951  exmidpeirce  16954  nninfall  16960  nninfsellemqall  16966  nninfsellemeqinf  16967  nninfomnilem  16969  nninfomni  16970  exmidsbthrlem  16975  sbthom  16979  isomninnlem  16987  isomninn  16988  cvgcmp2nlemabs  16989  iooreen  16992  trilpolemisumle  16995  trilpolemeq1  16997  trilpo  17000  trirec0  17001  apdifflemr  17004  qdiff  17006  iswomninnlem  17007  iswomninn  17008  ismkvnnlem  17010  ismkvnn  17011  redcwlpo  17013  dcapnconst  17019  nconstwlpolem0  17021  nconstwlpo  17024  neapmkv  17026  neap0mkv  17027  taupi  17031