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  4128  breqi  4136  breq1i  4137  breq2i  4138  brab1  4178  opabbii  4198  truni  4243  sepgi  4252  bm1.3ii  4254  a9evsep  4255  ax9vsep  4256  zfnuleu  4257  axnul  4258  ssexi  4271  difexi  4276  rabex  4280  rabex2  4282  elpw2  4293  pwnss  4296  iin0r  4306  intv  4307  pwex  4320  snex  4322  notnotsnex  4324  ord3ex  4327  dtruarb  4328  undifexmid  4330  intid  4364  opnzi  4375  copsexg  4384  opwo0id  4389  opelopabf  4417  epelc  4436  elon  4519  inton  4538  onn0  4545  onm  4546  elsuc  4551  elsuc2  4552  sucid  4562  iunsuc  4565  onordi  4571  ontrci  4572  onelssi  4574  eusvnf  4599  ssonunii  4636  sucex  4646  onssi  4662  onsuci  4663  ordtriexmidlem  4666  ordtriexmidlem2  4667  ordtriexmid  4668  ontriexmidim  4669  ordtri2orexmid  4670  2ordpr  4671  ontr2exmid  4672  onsucsssucexmid  4674  onsucelsucexmid  4677  regexmidlemm  4679  reg2exmid  4683  onirri  4690  ruALT  4698  onprc  4699  sucon  4700  dtru  4707  0elsucexmid  4712  ordpwsucexmid  4717  ordtri2or2exmid  4718  ontri2orexmidim  4719  dcextest  4728  omex  4740  find  4746  omelon  4756  nnoni  4758  limom  4761  nnregexmid  4768  omsinds  4769  xpeq1i  4794  xpeq2i  4795  0nelxp  4802  opthprc  4826  mosubop  4841  releqi  4858  relssi  4866  relin1  4895  relin2  4896  reldif  4897  inopab  4912  difopab  4913  xpiindim  4917  opabbi2dv  4929  ideq  4932  coeq1i  4939  coeq2i  4940  cnveqi  4955  eldm  4978  eldm2  4979  dmeqi  4982  dmv  4997  rneqi  5010  elrnmpti  5035  dmex  5049  rnex  5050  reseq1i  5059  reseq2i  5060  residm  5095  resex  5104  resmpt3  5112  imaeq1i  5123  imaeq2i  5124  elima  5131  imaex  5141  elimasn  5154  args  5156  epini  5158  dfse2  5160  eliniseg2  5167  relbrcnv  5168  cotr  5169  issref  5170  cnvsym  5171  asymref  5173  intirr  5174  codir  5176  qfto  5177  ssrnres  5230  cnveq0  5244  cnvsn0  5256  dmsnop  5261  rnsnop  5268  resdm2  5278  dfco2a  5288  cocnvcnv1  5298  coi2  5304  coires1  5305  cnvssrndm  5309  cossxp  5310  cocnvres  5312  relrelss  5314  relcoi2  5318  unidmrn  5320  dfdm2  5322  unixpm  5323  cnvexg  5325  cnvex  5326  cnviinm  5329  iotaval  5349  funeqi  5398  funi  5409  funres  5418  funcnvsn  5426  funcnvcnv  5440  funin  5452  funcnvres  5454  isarep2  5468  fneq1i  5475  fneq2i  5476  fndmi  5481  fnresdisj  5493  fnresi  5501  mpt0  5511  dmmpti  5513  feq1i  5526  feq2i  5527  fdmi  5541  fun2  5562  fssres  5565  resasplitss  5569  fintm  5577  fconst6  5592  f1ores  5654  foimacnv  5657  resdif  5661  funcocnv2  5664  f10d  5675  f1ovi  5680  fveq1i  5696  fveq2i  5698  0fv  5734  fvun1  5769  fvopab3ig  5779  fvmptss2  5780  mptrcl  5788  elfvmptrab1  5801  fndmdif  5814  fneqeql2  5818  f1oresrab  5873  fmptco  5874  funopsn  5891  fnressn  5901  fressnfv  5902  fmptap  5905  fvsnun1  5912  fvsnun2  5913  fsnunfv  5916  fconst2  5932  mptex  5943  fnfvimad  5954  rinvf1o  6035  riotabiia  6057  acexmidlema  6076  acexmidlemb  6077  acexmidlemcase  6080  acexmidlem2  6082  acexmidlemv  6083  oveq1i  6095  oveq2i  6096  oveqi  6098  oprabidlem  6116  0neqopab  6133  oprabbii  6143  oprabss  6174  mpompt  6180  funoprab  6188  fnoprab  6191  ovigg  6209  elmpocl  6284  relmptopab  6291  resfunexgALT  6337  cofunexg  6338  mptexw  6342  opabex3d  6350  opabex3  6351  1st0  6378  2nd0  6379  op1st  6380  op2nd  6381  f1stres  6393  f2ndres  6394  fo1stresm  6395  fo2ndresm  6396  1stcof  6397  2ndcof  6398  1stexg  6401  2ndexg  6402  releldm2  6419  reldm  6420  dfoprab3  6425  mpomptsx  6433  mpompts  6434  fnmpoi  6439  dmmpo  6440  mpoexxg  6446  mpoexw  6449  1stconst  6457  2ndconst  6458  dfmpo  6459  algrflem  6465  algrflemg  6466  cnvoprab  6470  f1od2  6471  elmpom  6474  mpoxopn0yelv  6510  mpoxopoveq  6511  tposssxp  6520  brtpos2  6522  reldmtpos  6524  dftpos2  6532  dftpos4  6534  tpostpos  6535  tpostpos2  6536  tposfo  6542  tposf  6543  tposeqi  6548  tposex  6549  tposoprab  6551  issmo  6559  smores  6563  smores2  6565  iordsmo  6568  smo0  6569  tfrlem8  6589  tfrexlem  6605  tfr1onlem3  6609  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlemres  6620  tfri1dALT  6622  tfri2  6637  rdgisuc1  6655  rdg0  6658  frecfun  6666  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecrdg  6679  2on0  6697  xp01disj  6706  2oconcl  6712  fnoa  6720  oaexg  6721  fnom  6723  omexg  6724  fnoei  6725  oeiexg  6726  oei0  6732  oacl  6733  oasuc  6737  o1p1e2  6741  omsuc  6745  nna0r  6751  nnm0r  6752  1onn  6793  2onn  6794  3onn  6795  4onn  6796  2ssom  6797  eqerlem  6838  eceq2i  6845  elqs  6860  qsex  6866  ecqs  6871  iinerm  6881  th3qlem1  6911  th3q  6914  mapsn  6972  mapsnf1o3  6979  ixpiinm  7006  ixpssmap  7014  brdom  7034  f1dom  7046  enref  7051  dom2  7061  idssen  7063  ssdomg  7065  ensymi  7069  ensn1  7083  fiprc  7104  1domsn  7115  dom1o  7116  xpcomf1o  7123  xpcomco  7124  dom0  7138  0dom  7139  xpmapenlem  7149  phplem2  7154  php5  7159  snnen2og  7160  1nen2  7162  php5dom  7164  ssfilem  7177  ssfiexmid  7178  ssfilemd  7179  ssfiexmidt  7180  domfiexmid  7182  0fi  7188  diffitest  7191  findcard  7192  findcard2  7193  findcard2s  7194  isinfinf  7201  ac6sfi  7202  inffiexmid  7213  pw1fin  7217  unfiexmid  7225  xpfi  7239  fisseneq  7242  ssfirab  7244  residfi  7254  mapfi  7261  en1eqsn  7265  snexxph  7267  sbthlem2  7275  sbthlemi3  7276  sbthlemi6  7279  sbthlem7  7280  fi0  7309  fipwfi  7322  supeq1i  7329  infeq1i  7354  djuexb  7385  djuf1olemr  7395  inresflem  7401  djuinr  7404  updjudhcoinlf  7421  updjudhcoinrg  7422  casefun  7426  caserel  7428  caseinj  7430  caseinl  7432  caseinr  7433  omp1eomlem  7435  endjusym  7437  difinfsn  7441  difinfinf  7442  djuinj  7447  0ct  7448  ctmlemr  7449  ctssdclemn0  7451  ctssdccl  7452  omct  7458  ctfoex  7459  finomni  7481  exmidomni  7483  fodjuomni  7490  ctssexmid  7491  fodjumkv  7501  nninfwlporlem  7514  nninfwlpoimlemg  7516  nninfwlpoim  7520  nninfinfwlpo  7521  card0  7534  ficardon  7535  exmidonfinlem  7546  dju1p1e2  7550  exmidfodomrlemim  7554  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  iftrueb01  7583  3nelsucpw1  7594  sucpw1nss3  7595  3nsssucpw1  7596  fmelpw1o  7607  2onetap  7622  exmidmotap  7628  0npi  7681  dmaddpi  7693  dmmulpi  7694  1lt2pi  7708  0nnq  7732  1nq  7734  dmaddpq  7747  dmmulpq  7748  rec1nq  7763  1lt2nq  7774  halfnqq  7778  prarloclemarch2  7787  enq0enq  7799  nqnq0pi  7806  nnnq0lem1  7814  addnnnq0  7817  mulnnnq0  7818  nq0m0r  7824  addpinq1  7832  prarloclem5  7868  prarloclemcalc  7870  1pr  7922  1idprl  7958  1idpru  7959  ltexprlemm  7968  recexprlem1ssl  8001  recexprlem1ssu  8002  suplocexprlemell  8081  suplocexprlem2b  8082  suplocexprlemmu  8086  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemub  8091  suplocexprlemlub  8092  prsrlem1  8110  addsrpr  8113  mulsrpr  8114  gt0srpr  8116  0nsr  8117  0r  8118  1sr  8119  m1r  8120  m1m1sr  8129  caucvgsr  8170  suplocsrlempr  8175  addresr  8205  mulresr  8206  pitonnlem1  8213  peano1nnnn  8220  axi2m1  8243  axcnre  8249  peano5nnnn  8260  axcaucvg  8268  mpomulf  8317  mulridi  8329  mullidi  8330  pnfnre  8368  mnfnre  8369  pnfnemnf  8381  mnfxr  8383  rexri  8384  ltnri  8420  ltleii  8430  00id  8469  addridi  8470  addlidi  8471  0cnALT  8518  negeqi  8522  negicn  8529  neg0  8574  renegcli  8590  negcli  8596  negidi  8597  negnegi  8598  subidi  8599  subid1i  8600  negne0bi  8601  negrebi  8602  mul02i  8719  mul01i  8720  mulm1i  8732  leidi  8815  gt0ne0ii  8817  inelr  8915  msqge0i  8948  gt0ap0ii  8959  1div1e1  9037  div1i  9073  eqnegi  9074  recclapi  9075  recidapi  9076  divmulapi  9099  rerecclapi  9110  redivclapi  9112  rerecapb  9176  recgt0  9183  ltp1i  9238  divgt0ii  9252  ltmul1ii  9261  ltdiv1ii  9262  sup3exmid  9290  indconst0  9305  indconst1  9306  peano5nni  9310  nnrei  9316  1nn  9318  nngt0i  9337  neg1ap0  9416  2timesi  9437  times2i  9438  2nn  9471  3nn  9472  4nn  9473  5nn  9474  6nn  9475  7nn  9476  8nn  9477  9nn  9478  2muline0  9535  rehalfcli  9559  nn0ssre  9572  nnnn0i  9576  dfn2  9581  0nn0  9583  nn0ge0i  9595  zrei  9655  neg1z  9681  nn0negzi  9684  dfz2  9722  nneoi  9755  peano5uzi  9760  dfuzi  9761  nn0ind-raph  9768  deceq1i  9788  deceq2i  9789  10nn  9801  numltc  9812  eluzel2  9936  eluz1i  9939  nn0uz  9967  nnuz  9968  uzuzle35  9975  infrenegsupex  10004  lbzbi  10026  divfnzn  10031  qdivcl  10053  irrmul  10058  irrmulap  10059  cnref1o  10062  0ltpnf  10195  mnflt0  10197  0lepnf  10203  xrltnsym  10206  xrlttri3  10210  nltpnft  10227  ngtmnft  10230  xrrebnd  10232  xnegmnf  10242  xneg0  10244  xltnegi  10248  xaddmnf1  10261  xaddmnf2  10262  mnfaddpnf  10264  xaddid1  10275  xnn0lenn0nn0  10278  xnn0xadd0  10280  xposdif  10295  ixxex  10312  iooval2  10328  unirnioo  10386  ioorebasg  10388  elrege0  10389  fzval2  10425  fzen  10458  fzprval  10500  fztpval  10501  uzdisj  10511  ige2m1fz  10528  fz01or  10529  fz1ssfz0  10535  fz0sn  10539  fz0tp  10540  fz0to3un2pr  10541  fz0to4untppr  10542  nn0disj  10556  1fv  10557  4fvwrd4  10558  fzo0ss1  10594  fzo01  10645  fzo12sn  10646  fzo0to2pr  10647  fzo0to3tp  10648  fzo0to42pr  10649  zsupssdc  10684  qbtwnxr  10703  flval  10718  flapcl  10722  flaplelt  10724  fldiv4lem1div2  10757  modqfrac  10789  modqmulnn  10794  q2txmodxeq0  10836  frecuzrdgdom  10870  frecuzrdgfun  10872  frecuzrdgsuct  10876  frechashgf1o  10880  nnct  10887  xnn0nnen  10889  fxnn0nninf  10891  0tonninf  10892  1tonninf  10893  iseqvalcbv  10911  ser0f  10986  0exp0e1  10996  qexpcl  11007  qexpclz  11012  m1expcl2  11013  1exp  11020  sqvali  11071  sqcli  11072  sqeq0i  11073  resqcli  11076  sq1  11085  neg1sqe1  11086  iexpcyc  11096  qsqeqor  11102  nn0sqdc  11162  facnn  11181  fac0  11182  fac1  11183  fac2  11185  fac3  11186  fac4  11187  bcval  11203  bcm1k  11214  bcpasc  11220  bccl  11221  4bc3eq4  11228  4bc2eq6  11229  hashinfom  11233  hashennn  11235  hashfz1  11238  fihasheq0  11248  hash0  11251  hashsng  11253  fihashen1  11254  en1hash  11255  omgadd  11258  hashp1i  11267  hashxp  11283  hashpwfi  11285  fimaxq  11286  ssenneg  11296  hashfibc  11299  hashf1lem1  11301  hashf1  11303  zfz1iso  11309  hash2en  11311  wrdexi  11333  wrdv  11336  wrdeqi  11343  wrd0  11345  lsw0  11368  ccatclab  11378  ccatidid  11394  s1prc  11407  ccat1st1st  11425  swrds1  11456  fnpfx  11465  swrdccatin2  11517  pfxccatin12lem2  11519  cats1fvn  11552  shftidt2  11613  cjexp  11674  re0  11677  im0  11678  re1  11679  im1  11680  cj0  11683  cji  11684  recli  11693  imcli  11694  cjcli  11695  replimi  11696  cjcji  11697  reim0bi  11698  rerebi  11699  cjrebi  11700  recji  11701  imcji  11702  cjmulrcli  11703  cjmulvali  11704  cjmulge0i  11705  renegi  11706  imnegi  11707  cjnegi  11708  addcji  11709  uzin2  11769  rexanuz  11770  rexfiuz  11771  sqrtrval  11782  sqrt0  11786  resqrexlemcalc3  11798  resqrexlemcvg  11801  resqrex  11808  abs0  11840  absi  11841  qabsor  11857  absimle  11867  recan  11892  caubnd2  11900  leabsi  11911  absrei  11912  sqrtpclii  11913  sqrtgt0ii  11914  absvalsqi  11923  absvalsq2i  11924  abscli  11925  absge0i  11926  absval2i  11927  abs00i  11928  absgt0api  11929  absnegi  11930  abscji  11931  releabsi  11932  infxrnegsupex  12048  xrbdtri  12061  cbvsum  12145  sumeq1i  12148  sum0  12174  isumz  12175  fisumss  12178  fsumsersdc  12181  fsumadd  12192  isumclim  12207  isumclim3  12209  fsumcnv  12223  modfsummodlem1  12242  fsumrelem  12257  binomlem  12269  binom  12270  arisum2  12285  expcnv  12290  0.999...  12307  prodf1f  12329  cbvprod  12344  prodeq1i  12347  zproddc  12365  zprodap0  12367  prod0  12371  fprodssdc  12376  prodsnf  12378  fprodcnv  12411  fprodge0  12423  fprodge1  12425  ef0lem  12446  esum  12448  ere  12456  ege2le3  12457  ef0  12458  eff2  12466  efsep  12477  reeff1  12486  sin0  12515  cos0  12516  ef01bndlem  12542  cos2bnd  12546  sincos1sgn  12551  sincos2sgn  12552  sin4lt0  12553  eirr  12565  0dvds  12597  dvds1  12639  z0even  12697  n2dvdsm1  12699  z2even  12700  n2dvds3  12701  ndvdssub  12716  ndvdsi  12719  flodddiv4  12722  bits0  12734  bitsfzo  12741  0bits  12745  m1bits  12746  bitsinv1lem  12747  bitsinv1  12748  gcddvds  12759  gcd1  12783  6gcd4e2  12791  bezoutlembi  12801  dfgcd3  12806  dfgcd2  12810  nninfctlemfo  12836  nninfct  12837  3lcm2e6woprm  12883  qredeu  12894  isprm2lem  12913  isprm3  12915  prm2orodd  12923  isprm5lem  12939  sqrt2irr0  12962  sqrtrirr  13008  phicl2  13015  phi1  13020  dfphi2  13021  phiprmpw  13023  eulerthlemrprm  13030  eulerthlemh  13032  odzval  13043  oddprm  13061  pczpre  13099  pcdiv  13104  pc0  13106  pcqdiv  13109  pcrec  13110  pcexp  13111  pcxcl  13113  pcxqcl  13114  pcdvdstr  13129  pc2dvds  13132  dvdsprmpweqnn  13138  pcmpt  13145  qexpz  13154  pockthi  13160  1arith2  13170  4sqlemffi  13198  4sqlem11  13203  4sqlem13m  13205  4sqlem19  13211  dec2dvds  13213  dec5nprm  13216  modxai  13218  modxp1i  13220  mod2xnegi  13221  numexp0  13225  numexp1  13226  1259lem5  13269  ballotfilem1  13272  ballotfilemonn  13273  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilem4  13293  ballotfilemi  13295  ballotfilem7  13331  ballotfilem8  13332  ballotfilemth  13333  ennnfonelemp1  13349  ennnfonelem1  13350  ennnfonelemkh  13355  ennnfonelemex  13357  ennnfonelemnn0  13365  ennnfonelemr  13366  exmidunben  13369  ctinfomlemom  13370  ctinfom  13371  ctinf  13373  qnnen  13374  omctfn  13386  omiunct  13387  ssnnctlemct  13389  nninfdc  13396  structcnvcnv  13420  structfun  13422  structfn  13423  ndxarg  13427  ndxid  13428  setsresg  13442  setsslnid  13456  basmex  13464  basmexd  13465  slotm  13467  strleun  13511  strle1g  13513  prdsvallem  13674  imasaddfnlemg  13688  quslem  13698  xpsfrnel  13718  xpsff1o  13723  ismgmn0  13731  fn0g  13748  0g0  13749  fngzsum  13761  idghm  14115  elcntr  14157  gsumsncmn  14240  gsumclfi  14243  gsummptfidmadd  14245  gsumsubmclfi  14247  gsumconstcmn  14250  prdsex  14256  prdsval  14257  prdsbaslemss  14258  mgpplusg  14306  mgpbas  14309  ringidval  14349  rhmfn  14563  rmodislmodlem  14771  rmodislmod  14772  lidlmex  14896  mopnset  14973  cntopex  14975  cnfldex  14980  cnfldbas  14981  mpocnfldadd  14982  mpocnfldmul  14984  cnfldcj  14986  cnfldtset  14987  cnfldle  14988  cnfldds  14989  cnring  14991  cnfld0  14992  cnfld1  14993  cnfldneg  14994  cnfldplusf  14995  cnfldsub  14996  cnfldmulg  14997  cnfldexp  14998  cnsubglem  15000  cnsubrglem  15001  gzsubrg  15003  gsumfsum  15007  cnfldui  15008  zringring  15012  zringabl  15013  zringgrp  15014  zring1  15020  zringsubgval  15024  expghmap  15026  znval  15055  znle  15056  znbaslemnn  15058  znbas  15063  znzrh2  15065  znzrhval  15066  znzrhfo  15067  znleval  15072  znidom  15076  znidomb  15077  fnpsr  15135  psrelbas  15151  psradd  15155  psraddcl  15156  psrmulfval  15159  psr1clfi  15170  mplrcl  15176  mplbasss  15178  mpladd  15186  istopon  15205  topontopi  15208  toponunii  15209  toponrestid  15213  istps  15224  topontopn  15229  eltpsi  15233  eltg4i  15247  eltg3  15249  tg1  15251  tg2  15252  tgclb  15257  topnex  15278  sn0topon  15280  distps  15283  cldrcl  15294  sn0cld  15329  restco  15366  lmrcl  15384  ssidcn  15402  cnconst2  15425  cnptopresti  15430  cnptoprest  15431  txuni2  15448  txbas  15450  eltx  15451  txcnp  15463  upxp  15464  txcnmpt  15465  uptx  15466  txcn  15467  txrest  15468  txlm  15471  cnmptid  15473  cnmpt1st  15480  cnmpt2nd  15481  hmeofn  15494  psmetge0  15523  ismeti  15538  xmetunirn  15550  xmetge0  15557  unirnblps  15614  unirnbl  15615  mopnex  15697  qtopbasss  15713  retop  15716  uniretop  15717  iooretopg  15720  cnxmet  15723  cntoptopon  15724  cnbl0  15726  cnfldxms  15729  cnfldtps  15730  rexmet  15741  blssioo  15745  tgioo  15746  tgqioo  15747  cnopnap  15803  hovercncf  15838  limcresi  15858  dvfvalap  15873  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvcnp2cntop  15891  dvcoapbr  15899  dvexp2  15904  dvrecap  15905  dveflem  15918  dvef  15919  plyun0  15928  plyrecj  15955  dvply2  15959  reeff1o  15965  sin0pilem1  15974  sin0pilem2  15975  pilem3  15976  pigt2lt4  15977  pire  15979  sinhalfpilem  15984  pidiv2halves  15988  cosneghalfpi  15991  cospi  15993  efipi  15994  sin2pi  15996  cos2pi  15997  ef2pi  15998  cosq14gt0  16025  coseq00topi  16028  coseq0negpitopi  16029  sincos4thpi  16033  sincos6thpi  16035  sincos3rdpi  16036  pigt3  16037  cos02pilt1  16044  ioocosf1o  16047  dfrelog  16053  relogf1o  16054  relogcl  16055  relogiso  16067  logfac  16090  rpcxpsqrt  16119  rpabscxpbnd  16137  2logb9irr  16168  2logb9irrALT  16171  sqrt2cxp2logb9e3  16172  2irrexpq  16173  2logb9irrap  16174  2irrexpqap  16175  log2tlbndlog2  16181  log2ublem2  16183  log2ublem3  16184  log2ublog2  16185  birthdaylog2  16189  prmdvdsfi  16204  ppiqp1le  16228  ppi1  16231  cht1  16232  cht2  16237  ppiqnncl  16239  chtqrpcl  16240  ppiqeq0  16241  ppiqltx  16242  prmorcht  16243  mpodvdsmulf1o  16245  fsumdvdsmul  16246  ppiublem1  16252  ppiublem2  16253  ppiqub  16254  chtublem  16256  chtqub  16257  perfectlem2  16261  bclbnd  16268  bpos1lem  16270  bposlem4  16275  bposlem5  16276  bposlem6  16277  bposlem7  16278  bposlem8  16279  bposlem9  16280  lgsdir2lem1  16313  lgsdir2lem2  16314  lgsdir2lem4  16316  lgsdir2lem5  16317  lgsdi  16322  gausslemma2dlem0i  16342  gausslemma2dlem4  16349  lgseisenlem4  16358  lgsquadlem1  16362  lgsquad2lem2  16367  lgsquad2  16368  m1lgs  16370  2lgs2  16387  2lgslem4  16388  2lgsoddprmlem2  16391  2lgsoddprmlem3c  16394  2lgsoddprmlem3d  16395  2sqlem9  16409  2sqlem10  16410  1vgrex  16427  vtxval0  16460  iedgval0  16461  uhgr0  16492  upgrfi  16509  umgrislfupgrdom  16538  ausgrusgrben  16575  uspgredgiedg  16585  uspgriedgedg  16586  usgrislfuspgrdom  16597  uspgredg2vlem  16627  uspgredg2v  16628  usgr0  16646  griedg0prc  16657  subupgr  16680  vdegp1cid  16723  0wlk0  16778  clwwlkn1  16825  clwwlkn2  16828  eupth2lem1  16865  eulerpathum  16888  konigsbergiedgwen  16891  konigsberglem1  16895  konigsberglem3  16897  konigsberglem4  16898  konigsberglem5  16899  konigsberg  16900  ex-fl  16905  ex-ceil  16906  ex-exp  16907  ex-fac  16908  ex-gcd  16911  bj-stfal  16936  bj-stst  16939  bj-dcfal  16949  bj-dcdc  16953  bj-stdc  16954  bj-dcst  16955  bj-el2oss1o  16968  elabf2  16976  bd0  17016  bdeli  17038  bdcriota  17075  bdbm1.3ii  17083  bdinex1  17091  bdssexi  17095  bj-inex  17099  bj-snex  17105  bj-sucex  17115  bj-d0clsepcl  17117  bj-omind  17126  bj-om  17129  bj-2inf  17130  bj-peano2  17131  bdpeano5  17135  bj-omssonALT  17155  bj-inf2vnlem1  17162  bj-omex2  17169  bj-nn0sucALT  17170  3dom  17184  012of  17189  2o01f  17190  subctctexmid  17196  pw1dceq  17201  exmidpeirce  17204  wexmiddc  17208  wexmiddiffilem  17209  wexmiddifxylem  17211  wexmiddifxy  17212  nninfall  17218  nninfsellemqall  17224  nninfsellemeqinf  17225  nninfomnilem  17227  nninfomni  17228  exmidsbthrlem  17233  sbthom  17237  isomninnlem  17245  isomninn  17246  cvgcmp2nlemabs  17247  iooreen  17250  trilpolemisumle  17254  trilpolemeq1  17256  trilpo  17259  trirec0  17260  apdifflemr  17263  qdiff  17265  iswomninnlem  17266  iswomninn  17267  ismkvnnlem  17269  ismkvnn  17270  redcwlpo  17272  dcapnconst  17278  nconstwlpolem0  17280  nconstwlpo  17283  neapmkv  17285  neap0mkv  17286  taupi  17290