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  7321  supeq1i  7328  infeq1i  7353  djuexb  7384  djuf1olemr  7394  inresflem  7400  djuinr  7403  updjudhcoinlf  7420  updjudhcoinrg  7421  casefun  7425  caserel  7427  caseinj  7429  caseinl  7431  caseinr  7432  omp1eomlem  7434  endjusym  7436  difinfsn  7440  difinfinf  7441  djuinj  7446  0ct  7447  ctmlemr  7448  ctssdclemn0  7450  ctssdccl  7451  omct  7457  ctfoex  7458  finomni  7480  exmidomni  7482  fodjuomni  7489  ctssexmid  7490  fodjumkv  7500  nninfwlporlem  7513  nninfwlpoimlemg  7515  nninfwlpoim  7519  nninfinfwlpo  7520  card0  7533  ficardon  7534  exmidonfinlem  7545  dju1p1e2  7549  exmidfodomrlemim  7553  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  iftrueb01  7582  3nelsucpw1  7593  sucpw1nss3  7594  3nsssucpw1  7595  fmelpw1o  7606  2onetap  7621  exmidmotap  7627  0npi  7680  dmaddpi  7692  dmmulpi  7693  1lt2pi  7707  0nnq  7731  1nq  7733  dmaddpq  7746  dmmulpq  7747  rec1nq  7762  1lt2nq  7773  halfnqq  7777  prarloclemarch2  7786  enq0enq  7798  nqnq0pi  7805  nnnq0lem1  7813  addnnnq0  7816  mulnnnq0  7817  nq0m0r  7823  addpinq1  7831  prarloclem5  7867  prarloclemcalc  7869  1pr  7921  1idprl  7957  1idpru  7958  ltexprlemm  7967  recexprlem1ssl  8000  recexprlem1ssu  8001  suplocexprlemell  8080  suplocexprlem2b  8081  suplocexprlemmu  8085  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexprlemlub  8091  prsrlem1  8109  addsrpr  8112  mulsrpr  8113  gt0srpr  8115  0nsr  8116  0r  8117  1sr  8118  m1r  8119  m1m1sr  8128  caucvgsr  8169  suplocsrlempr  8174  addresr  8204  mulresr  8205  pitonnlem1  8212  peano1nnnn  8219  axi2m1  8242  axcnre  8248  peano5nnnn  8259  axcaucvg  8267  mpomulf  8316  mulridi  8328  mullidi  8329  pnfnre  8367  mnfnre  8368  pnfnemnf  8380  mnfxr  8382  rexri  8383  ltnri  8419  ltleii  8429  00id  8468  addridi  8469  addlidi  8470  0cnALT  8517  negeqi  8521  negicn  8528  neg0  8573  renegcli  8589  negcli  8595  negidi  8596  negnegi  8597  subidi  8598  subid1i  8599  negne0bi  8600  negrebi  8601  mul02i  8718  mul01i  8719  mulm1i  8731  leidi  8814  gt0ne0ii  8816  inelr  8914  msqge0i  8947  gt0ap0ii  8958  1div1e1  9036  div1i  9072  eqnegi  9073  recclapi  9074  recidapi  9075  divmulapi  9098  rerecclapi  9109  redivclapi  9111  rerecapb  9175  recgt0  9182  ltp1i  9237  divgt0ii  9251  ltmul1ii  9260  ltdiv1ii  9261  sup3exmid  9289  indconst0  9304  indconst1  9305  peano5nni  9309  nnrei  9315  1nn  9317  nngt0i  9336  neg1ap0  9415  2timesi  9436  times2i  9437  2nn  9470  3nn  9471  4nn  9472  5nn  9473  6nn  9474  7nn  9475  8nn  9476  9nn  9477  2muline0  9534  rehalfcli  9558  nn0ssre  9571  nnnn0i  9575  dfn2  9580  0nn0  9582  nn0ge0i  9594  zrei  9654  neg1z  9680  nn0negzi  9683  dfz2  9721  nneoi  9754  peano5uzi  9759  dfuzi  9760  nn0ind-raph  9767  deceq1i  9787  deceq2i  9788  10nn  9800  numltc  9811  eluzel2  9935  eluz1i  9938  nn0uz  9966  nnuz  9967  uzuzle35  9974  infrenegsupex  10003  lbzbi  10025  divfnzn  10030  qdivcl  10052  irrmul  10057  irrmulap  10058  cnref1o  10061  0ltpnf  10194  mnflt0  10196  0lepnf  10202  xrltnsym  10205  xrlttri3  10209  nltpnft  10226  ngtmnft  10229  xrrebnd  10231  xnegmnf  10241  xneg0  10243  xltnegi  10247  xaddmnf1  10260  xaddmnf2  10261  mnfaddpnf  10263  xaddid1  10274  xnn0lenn0nn0  10277  xnn0xadd0  10279  xposdif  10294  ixxex  10311  iooval2  10327  unirnioo  10385  ioorebasg  10387  elrege0  10388  fzval2  10424  fzen  10457  fzprval  10499  fztpval  10500  uzdisj  10510  ige2m1fz  10527  fz01or  10528  fz1ssfz0  10534  fz0sn  10538  fz0tp  10539  fz0to3un2pr  10540  fz0to4untppr  10541  nn0disj  10555  1fv  10556  4fvwrd4  10557  fzo0ss1  10593  fzo01  10644  fzo12sn  10645  fzo0to2pr  10646  fzo0to3tp  10647  fzo0to42pr  10648  zsupssdc  10683  qbtwnxr  10702  flval  10717  flapcl  10721  flaplelt  10723  fldiv4lem1div2  10755  modqfrac  10787  modqmulnn  10792  q2txmodxeq0  10834  frecuzrdgdom  10868  frecuzrdgfun  10870  frecuzrdgsuct  10874  frechashgf1o  10878  nnct  10885  xnn0nnen  10887  fxnn0nninf  10889  0tonninf  10890  1tonninf  10891  iseqvalcbv  10909  ser0f  10984  0exp0e1  10994  qexpcl  11005  qexpclz  11010  m1expcl2  11011  1exp  11018  sqvali  11069  sqcli  11070  sqeq0i  11071  resqcli  11074  sq1  11083  neg1sqe1  11084  iexpcyc  11094  qsqeqor  11100  nn0sqdc  11160  facnn  11179  fac0  11180  fac1  11181  fac2  11183  fac3  11184  fac4  11185  bcval  11201  bcm1k  11212  bcpasc  11218  bccl  11219  4bc3eq4  11226  4bc2eq6  11227  hashinfom  11231  hashennn  11233  hashfz1  11236  fihasheq0  11246  hash0  11249  hashsng  11251  fihashen1  11252  en1hash  11253  omgadd  11256  hashp1i  11265  hashxp  11281  hashpwfi  11283  fimaxq  11284  ssenneg  11294  hashfibc  11297  hashf1lem1  11299  hashf1  11301  zfz1iso  11307  hash2en  11309  wrdexi  11331  wrdv  11334  wrdeqi  11341  wrd0  11343  lsw0  11366  ccatclab  11376  ccatidid  11392  s1prc  11405  ccat1st1st  11423  swrds1  11454  fnpfx  11463  swrdccatin2  11515  pfxccatin12lem2  11517  cats1fvn  11550  shftidt2  11611  cjexp  11672  re0  11675  im0  11676  re1  11677  im1  11678  cj0  11681  cji  11682  recli  11691  imcli  11692  cjcli  11693  replimi  11694  cjcji  11695  reim0bi  11696  rerebi  11697  cjrebi  11698  recji  11699  imcji  11700  cjmulrcli  11701  cjmulvali  11702  cjmulge0i  11703  renegi  11704  imnegi  11705  cjnegi  11706  addcji  11707  uzin2  11767  rexanuz  11768  rexfiuz  11769  sqrtrval  11780  sqrt0  11784  resqrexlemcalc3  11796  resqrexlemcvg  11799  resqrex  11806  abs0  11838  absi  11839  qabsor  11855  absimle  11865  recan  11890  caubnd2  11898  leabsi  11909  absrei  11910  sqrtpclii  11911  sqrtgt0ii  11912  absvalsqi  11921  absvalsq2i  11922  abscli  11923  absge0i  11924  absval2i  11925  abs00i  11926  absgt0api  11927  absnegi  11928  abscji  11929  releabsi  11930  infxrnegsupex  12045  xrbdtri  12058  cbvsum  12142  sumeq1i  12145  sum0  12171  isumz  12172  fisumss  12175  fsumsersdc  12178  fsumadd  12189  isumclim  12204  isumclim3  12206  fsumcnv  12220  modfsummodlem1  12239  fsumrelem  12254  binomlem  12266  binom  12267  arisum2  12282  expcnv  12287  0.999...  12304  prodf1f  12326  cbvprod  12341  prodeq1i  12344  zproddc  12362  zprodap0  12364  prod0  12368  fprodssdc  12373  prodsnf  12375  fprodcnv  12408  fprodge0  12420  fprodge1  12422  ef0lem  12443  esum  12445  ere  12453  ege2le3  12454  ef0  12455  eff2  12463  efsep  12474  reeff1  12483  sin0  12512  cos0  12513  ef01bndlem  12539  cos2bnd  12543  sincos1sgn  12548  sincos2sgn  12549  sin4lt0  12550  eirr  12562  0dvds  12594  dvds1  12636  z0even  12694  n2dvdsm1  12696  z2even  12697  n2dvds3  12698  ndvdssub  12713  ndvdsi  12716  flodddiv4  12719  bits0  12731  bitsfzo  12738  0bits  12742  m1bits  12743  bitsinv1lem  12744  bitsinv1  12745  gcddvds  12756  gcd1  12780  6gcd4e2  12788  bezoutlembi  12798  dfgcd3  12803  dfgcd2  12807  nninfctlemfo  12833  nninfct  12834  3lcm2e6woprm  12880  qredeu  12891  isprm2lem  12910  isprm3  12912  prm2orodd  12920  isprm5lem  12936  sqrt2irr0  12959  sqrtrirr  13005  phicl2  13012  phi1  13017  dfphi2  13018  phiprmpw  13020  eulerthlemrprm  13027  eulerthlemh  13029  odzval  13040  oddprm  13058  pczpre  13096  pcdiv  13101  pc0  13103  pcqdiv  13106  pcrec  13107  pcexp  13108  pcxcl  13110  pcxqcl  13111  pcdvdstr  13126  pc2dvds  13129  dvdsprmpweqnn  13135  pcmpt  13142  qexpz  13151  pockthi  13157  1arith2  13167  4sqlemffi  13195  4sqlem11  13200  4sqlem13m  13202  4sqlem19  13208  dec2dvds  13210  dec5nprm  13213  modxai  13215  modxp1i  13217  mod2xnegi  13218  numexp0  13222  numexp1  13223  1259lem5  13266  ballotfilem1  13269  ballotfilemonn  13270  ballotfilem2  13277  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilem4  13290  ballotfilemi  13292  ballotfilem7  13328  ballotfilem8  13329  ballotfilemth  13330  ennnfonelemp1  13346  ennnfonelem1  13347  ennnfonelemkh  13352  ennnfonelemex  13354  ennnfonelemnn0  13362  ennnfonelemr  13363  exmidunben  13366  ctinfomlemom  13367  ctinfom  13368  ctinf  13370  qnnen  13371  omctfn  13383  omiunct  13384  ssnnctlemct  13386  nninfdc  13393  structcnvcnv  13417  structfun  13419  structfn  13420  ndxarg  13424  ndxid  13425  setsresg  13439  setsslnid  13453  basmex  13461  basmexd  13462  slotm  13464  strleun  13507  strle1g  13509  prdsvallem  13670  imasaddfnlemg  13684  quslem  13694  xpsfrnel  13714  xpsff1o  13719  ismgmn0  13727  fn0g  13744  0g0  13745  fngzsum  13757  idghm  14111  gsumsncmn  14205  gsumclfi  14208  gsummptfidmadd  14210  gsumsubmclfi  14212  gsumconstcmn  14215  prdsex  14221  prdsval  14222  prdsbaslemss  14223  mgpplusg  14271  mgpbas  14274  ringidval  14314  rhmfn  14528  rmodislmodlem  14736  rmodislmod  14737  lidlmex  14861  mopnset  14938  cntopex  14940  cnfldex  14945  cnfldbas  14946  mpocnfldadd  14947  mpocnfldmul  14949  cnfldcj  14951  cnfldtset  14952  cnfldle  14953  cnfldds  14954  cnring  14956  cnfld0  14957  cnfld1  14958  cnfldneg  14959  cnfldplusf  14960  cnfldsub  14961  cnfldmulg  14962  cnfldexp  14963  cnsubglem  14965  cnsubrglem  14966  gzsubrg  14968  gsumfsum  14972  cnfldui  14973  zringring  14977  zringabl  14978  zringgrp  14979  zring1  14985  zringsubgval  14989  expghmap  14991  znval  15020  znle  15021  znbaslemnn  15023  znbas  15028  znzrh2  15030  znzrhval  15031  znzrhfo  15032  znleval  15037  znidom  15041  znidomb  15042  fnpsr  15100  psrelbas  15115  psradd  15119  psraddcl  15120  psr1clfi  15128  mplrcl  15134  mplbasss  15136  mpladd  15144  istopon  15163  topontopi  15166  toponunii  15167  toponrestid  15171  istps  15182  topontopn  15187  eltpsi  15191  eltg4i  15205  eltg3  15207  tg1  15209  tg2  15210  tgclb  15215  topnex  15236  sn0topon  15238  distps  15241  cldrcl  15252  sn0cld  15287  restco  15324  lmrcl  15342  ssidcn  15360  cnconst2  15383  cnptopresti  15388  cnptoprest  15389  txuni2  15406  txbas  15408  eltx  15409  txcnp  15421  upxp  15422  txcnmpt  15423  uptx  15424  txcn  15425  txrest  15426  txlm  15429  cnmptid  15431  cnmpt1st  15438  cnmpt2nd  15439  hmeofn  15452  psmetge0  15481  ismeti  15496  xmetunirn  15508  xmetge0  15515  unirnblps  15572  unirnbl  15573  mopnex  15655  qtopbasss  15671  retop  15674  uniretop  15675  iooretopg  15678  cnxmet  15681  cntoptopon  15682  cnbl0  15684  cnfldxms  15687  cnfldtps  15688  rexmet  15699  blssioo  15703  tgioo  15704  tgqioo  15705  cnopnap  15761  hovercncf  15796  limcresi  15816  dvfvalap  15831  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvcnp2cntop  15849  dvcoapbr  15857  dvexp2  15862  dvrecap  15863  dveflem  15876  dvef  15877  plyun0  15886  plyrecj  15913  dvply2  15917  reeff1o  15923  sin0pilem1  15932  sin0pilem2  15933  pilem3  15934  pigt2lt4  15935  pire  15937  sinhalfpilem  15942  pidiv2halves  15946  cosneghalfpi  15949  cospi  15951  efipi  15952  sin2pi  15954  cos2pi  15955  ef2pi  15956  cosq14gt0  15983  coseq00topi  15986  coseq0negpitopi  15987  sincos4thpi  15991  sincos6thpi  15993  sincos3rdpi  15994  pigt3  15995  cos02pilt1  16002  ioocosf1o  16005  dfrelog  16011  relogf1o  16012  relogcl  16013  relogiso  16025  logfac  16048  rpcxpsqrt  16077  rpabscxpbnd  16095  2logb9irr  16126  2logb9irrALT  16129  sqrt2cxp2logb9e3  16130  2irrexpq  16131  2logb9irrap  16132  2irrexpqap  16133  log2tlbndlog2  16139  log2ublem2  16141  log2ublem3  16142  log2ublog2  16143  birthdaylog2  16147  prmdvdsfi  16159  ppiqp1le  16173  ppi1  16176  ppiqnncl  16181  ppiqeq0  16182  ppiqltx  16183  mpodvdsmulf1o  16185  fsumdvdsmul  16186  ppiublem1  16192  ppiublem2  16193  ppiqub  16194  perfectlem2  16198  bclbnd  16205  bpos1lem  16207  bposlem4  16212  bposlem5  16213  lgsdir2lem1  16245  lgsdir2lem2  16246  lgsdir2lem4  16248  lgsdir2lem5  16249  lgsdi  16254  gausslemma2dlem0i  16274  gausslemma2dlem4  16281  lgseisenlem4  16290  lgsquadlem1  16294  lgsquad2lem2  16299  lgsquad2  16300  m1lgs  16302  2lgs2  16319  2lgslem4  16320  2lgsoddprmlem2  16323  2lgsoddprmlem3c  16326  2lgsoddprmlem3d  16327  2sqlem9  16341  2sqlem10  16342  1vgrex  16359  vtxval0  16392  iedgval0  16393  uhgr0  16424  upgrfi  16441  umgrislfupgrdom  16470  ausgrusgrben  16507  uspgredgiedg  16517  uspgriedgedg  16518  usgrislfuspgrdom  16529  uspgredg2vlem  16559  uspgredg2v  16560  usgr0  16578  griedg0prc  16589  subupgr  16612  vdegp1cid  16655  0wlk0  16710  clwwlkn1  16757  clwwlkn2  16760  eupth2lem1  16797  eulerpathum  16820  konigsbergiedgwen  16823  konigsberglem1  16827  konigsberglem3  16829  konigsberglem4  16830  konigsberglem5  16831  konigsberg  16832  ex-fl  16837  ex-ceil  16838  ex-exp  16839  ex-fac  16840  ex-gcd  16843  bj-stfal  16868  bj-stst  16871  bj-dcfal  16881  bj-dcdc  16885  bj-stdc  16886  bj-dcst  16887  bj-el2oss1o  16900  elabf2  16908  bd0  16948  bdeli  16970  bdcriota  17007  bdbm1.3ii  17015  bdinex1  17023  bdssexi  17027  bj-inex  17031  bj-snex  17037  bj-sucex  17047  bj-d0clsepcl  17049  bj-omind  17058  bj-om  17061  bj-2inf  17062  bj-peano2  17063  bdpeano5  17067  bj-omssonALT  17087  bj-inf2vnlem1  17094  bj-omex2  17101  bj-nn0sucALT  17102  3dom  17116  012of  17121  2o01f  17122  subctctexmid  17128  pw1dceq  17133  exmidpeirce  17136  wexmiddc  17140  wexmiddiffilem  17141  wexmiddifxylem  17143  wexmiddifxy  17144  nninfall  17150  nninfsellemqall  17156  nninfsellemeqinf  17157  nninfomnilem  17159  nninfomni  17160  exmidsbthrlem  17165  sbthom  17169  isomninnlem  17177  isomninn  17178  cvgcmp2nlemabs  17179  iooreen  17182  trilpolemisumle  17185  trilpolemeq1  17187  trilpo  17190  trirec0  17191  apdifflemr  17194  qdiff  17196  iswomninnlem  17197  iswomninn  17198  ismkvnnlem  17200  ismkvnn  17201  redcwlpo  17203  dcapnconst  17209  nconstwlpolem0  17211  nconstwlpo  17214  neapmkv  17216  neap0mkv  17217  taupi  17221