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 666.

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  642  notnoti  648  pm2.21i  649  pm2.24ii  650  notbii  672  nbn  704  ori  728  orci  736  olci  737  biorfi  751  imorri  754  dcbii  845  simp1i  1030  simp2i  1031  simp3i  1032  3mix1i  1193  3mix2i  1194  3mix3i  1195  3jaoi  1337  mptru  1404  dfnot  1413  mptnan  1465  mtpor  1467  mtpxor  1468  dcfromnotnotr  1490  dcfromcon  1491  dcfrompeirce  1492  mpg  1497  19.23h  1544  hbequid  1559  axi12  1560  nfri  1565  spi  1582  19.21  1629  eximii  1648  19.35i  1671  nfn  1704  19.37aiv  1721  19.23  1724  exan  1739  equid  1747  hbae  1764  equvini  1804  equveli  1805  sbid  1820  sbieh  1836  exdistrfor  1846  dveeq2or  1862  ax11v  1873  ax11ev  1874  equs5or  1876  sb4or  1879  sb4bor  1881  nfsb2or  1883  sbequilem  1884  sbequi  1885  speiv  1908  nfsbxy  1993  nfsbxyt  1994  sbco  2019  sbcocom  2021  sbcomxyyz  2023  sbal1yz  2052  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  eumoi  2110  moani  2148  elsb1  2207  elsb2  2208  eqeq1i  2237  eqeq2i  2240  eleq1i  2295  eleq2i  2296  nfcrii  2365  neeq1i  2415  neeq2i  2416  necon3i  2448  rspec  2582  rgen2a  2584  mprg  2587  r19.21  2606  r19.23  2639  raleqi  2732  rexeqi  2733  rabeqif  2791  elv  2804  elexi  2813  ceqsal  2830  vtocl3  2858  vtoclef  2877  vtocle  2878  spcv  2898  spcev  2899  clel3  2939  elabf  2947  elab2  2952  elab3  2956  euxfrdc  2990  reueq  3003  rmoimi2  3007  sbsbc  3033  sbc8g  3037  sbc6  3055  sbcie  3064  sbcrex  3109  csbvarg  3153  csbief  3170  csbie2  3175  sbnfc2  3186  sseli  3221  sselii  3222  sseq1i  3251  sseq2i  3252  difeq1i  3319  difeq2i  3320  uneq1i  3355  uneq2i  3356  ineq1i  3402  ineq2i  3403  ssinss1  3434  difdif2ss  3462  n0ii  3501  ne0ii  3502  vn0  3503  vn0m  3504  abf  3536  disj2  3548  difid  3561  0dif  3564  disjdif  3565  difin0  3566  undif1ss  3567  difdifdirss  3577  iftruei  3609  iffalsei  3612  ifbieq2i  3627  ifbieq12i  3629  pweqi  3654  pwid  3665  sneqi  3679  elsn  3683  elpr  3688  elsn2  3701  ralsn  3710  rexsn  3711  eltp  3715  rabrsndc  3737  preq1i  3749  preq2i  3750  prid1  3775  snnz  3789  snm  3790  prnz  3793  prm  3794  tpnz  3796  snss  3806  snsssn  3842  opeq1i  3863  opeq2i  3864  unieqi  3901  unissi  3914  inteqi  3930  intmin2  3952  intab  3955  intsn  3961  iinconstm  3977  iuniin  3978  iinss1  3980  iunxdif2  4017  ssiinf  4018  iinss  4020  iinss2  4021  iinab  4030  iundif2ss  4034  iindif2m  4036  iinin2m  4037  iunxsn  4045  iunxprg  4049  iinpw  4059  invdisjrab  4080  sndisj  4082  disjxsn  4084  breqi  4092  breq1i  4093  breq2i  4094  brab1  4134  opabbii  4154  truni  4199  bm1.3ii  4208  a9evsep  4209  ax9vsep  4210  zfnuleu  4211  axnul  4212  ssexi  4225  rabex  4232  rabex2  4234  elpw2  4245  pwnss  4247  iin0r  4257  intv  4258  pwex  4271  snex  4273  notnotsnex  4275  ord3ex  4278  dtruarb  4279  undifexmid  4281  intid  4314  opnzi  4325  copsexg  4334  opwo0id  4339  opelopabf  4367  epelc  4386  elon  4469  inton  4488  onn0  4495  onm  4496  elsuc  4501  elsuc2  4502  sucid  4512  iunsuc  4515  onordi  4521  ontrci  4522  onelssi  4524  eusvnf  4548  ssonunii  4585  sucex  4595  onssi  4611  onsuci  4612  ordtriexmidlem  4615  ordtriexmidlem2  4616  ordtriexmid  4617  ontriexmidim  4618  ordtri2orexmid  4619  2ordpr  4620  ontr2exmid  4621  onsucsssucexmid  4623  onsucelsucexmid  4626  regexmidlemm  4628  reg2exmid  4632  onirri  4639  ruALT  4647  onprc  4648  sucon  4649  dtru  4656  0elsucexmid  4661  ordpwsucexmid  4666  ordtri2or2exmid  4667  ontri2orexmidim  4668  dcextest  4677  omex  4689  find  4695  omelon  4705  nnoni  4707  limom  4710  nnregexmid  4717  omsinds  4718  xpeq1i  4743  xpeq2i  4744  0nelxp  4751  opthprc  4775  mosubop  4790  releqi  4807  relssi  4815  relin1  4843  relin2  4844  reldif  4845  inopab  4860  difopab  4861  xpiindim  4865  opabbi2dv  4877  ideq  4880  coeq1i  4887  coeq2i  4888  cnveqi  4903  eldm  4926  eldm2  4927  dmeqi  4930  dmv  4945  rneqi  4958  elrnmpti  4983  dmex  4997  rnex  4998  reseq1i  5007  reseq2i  5008  residm  5043  resex  5052  resmpt3  5060  imaeq1i  5071  imaeq2i  5072  elima  5079  imaex  5089  elimasn  5101  args  5103  epini  5105  dfse2  5107  eliniseg2  5114  relbrcnv  5115  cotr  5116  issref  5117  cnvsym  5118  asymref  5120  intirr  5121  codir  5123  qfto  5124  ssrnres  5177  cnveq0  5191  cnvsn0  5203  dmsnop  5208  rnsnop  5215  resdm2  5225  dfco2a  5235  cocnvcnv1  5245  coi2  5251  coires1  5252  cnvssrndm  5256  cossxp  5257  cocnvres  5259  relrelss  5261  relcoi2  5265  unidmrn  5267  dfdm2  5269  unixpm  5270  cnvexg  5272  cnvex  5273  cnviinm  5276  iotaval  5296  funeqi  5345  funi  5356  funres  5365  funcnvsn  5372  funcnvcnv  5386  funin  5398  funcnvres  5400  isarep2  5414  fneq1i  5421  fneq2i  5422  fndmi  5427  fnresdisj  5439  fnresi  5447  mpt0  5457  dmmpti  5459  feq1i  5472  feq2i  5473  fdmi  5487  fun2  5506  fssres  5509  resasplitss  5513  fintm  5519  fconst6  5533  f1ores  5595  foimacnv  5598  resdif  5602  funcocnv2  5605  f10d  5615  f1ovi  5620  fveq1i  5636  fveq2i  5638  0fv  5673  fvun1  5708  fvopab3ig  5716  fvmptss2  5717  mptrcl  5725  elfvmptrab1  5737  fndmdif  5748  fneqeql2  5752  f1oresrab  5808  fmptco  5809  funopsn  5825  fnressn  5835  fressnfv  5836  fmptap  5839  fvsnun1  5846  fvsnun2  5847  fsnunfv  5850  fconst2  5866  mptex  5875  fnfvimad  5885  riotabiia  5985  acexmidlema  6004  acexmidlemb  6005  acexmidlemcase  6008  acexmidlem2  6010  acexmidlemv  6011  oveq1i  6023  oveq2i  6024  oveqi  6026  oprabidlem  6044  0neqopab  6061  oprabbii  6071  oprabss  6102  mpompt  6108  funoprab  6116  fnoprab  6119  ovigg  6137  elmpocl  6212  relmptopab  6219  resfunexgALT  6265  cofunexg  6266  mptexw  6270  opabex3d  6278  opabex3  6279  1st0  6302  2nd0  6303  op1st  6304  op2nd  6305  f1stres  6317  f2ndres  6318  fo1stresm  6319  fo2ndresm  6320  1stcof  6321  2ndcof  6322  1stexg  6325  2ndexg  6326  releldm2  6343  reldm  6344  dfoprab3  6349  mpomptsx  6357  mpompts  6358  fnmpoi  6363  dmmpo  6364  mpoexxg  6370  mpoexw  6373  1stconst  6381  2ndconst  6382  dfmpo  6383  algrflem  6389  algrflemg  6390  cnvoprab  6394  f1od2  6395  elmpom  6398  mpoxopn0yelv  6400  mpoxopoveq  6401  tposssxp  6410  brtpos2  6412  reldmtpos  6414  dftpos2  6422  dftpos4  6424  tpostpos  6425  tpostpos2  6426  tposfo  6432  tposf  6433  tposeqi  6438  tposex  6439  tposoprab  6441  issmo  6449  smores  6453  smores2  6455  iordsmo  6458  smo0  6459  tfrlem8  6479  tfrexlem  6495  tfr1onlem3  6499  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlemres  6510  tfri1dALT  6512  tfri2  6527  rdgisuc1  6545  rdg0  6548  frecfun  6556  frec0g  6558  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecrdg  6569  2on0  6587  xp01disj  6596  2oconcl  6602  fnoa  6610  oaexg  6611  fnom  6613  omexg  6614  fnoei  6615  oeiexg  6616  oei0  6622  oacl  6623  oasuc  6627  o1p1e2  6631  omsuc  6635  nna0r  6641  nnm0r  6642  1onn  6683  2onn  6684  3onn  6685  4onn  6686  2ssom  6687  eqerlem  6728  eceq2i  6735  elqs  6750  qsex  6756  ecqs  6761  iinerm  6771  th3qlem1  6801  th3q  6804  mapsn  6854  mapsnf1o3  6861  ixpiinm  6888  ixpssmap  6896  brdom  6916  f1dom  6928  enref  6933  dom2  6943  idssen  6945  ssdomg  6947  ensymi  6951  ensn1  6965  fiprc  6985  1domsn  6996  dom1o  6997  xpcomf1o  7004  xpcomco  7005  dom0  7019  0dom  7020  xpmapenlem  7030  phplem2  7034  php5  7039  snnen2og  7040  1nen2  7042  php5dom  7044  ssfilem  7057  ssfiexmid  7058  domfiexmid  7060  0fi  7066  diffitest  7069  findcard  7070  findcard2  7071  findcard2s  7072  isinfinf  7079  ac6sfi  7080  inffiexmid  7091  pw1fin  7095  unfiexmid  7103  xpfi  7117  fisseneq  7119  ssfirab  7121  residfi  7130  en1eqsn  7138  snexxph  7140  sbthlem2  7148  sbthlemi3  7149  sbthlemi6  7152  sbthlem7  7153  fi0  7165  supeq1i  7178  infeq1i  7203  djuexb  7234  djuf1olemr  7244  inresflem  7250  djuinr  7253  updjudhcoinlf  7270  updjudhcoinrg  7271  casefun  7275  caserel  7277  caseinj  7279  caseinl  7281  caseinr  7282  omp1eomlem  7284  endjusym  7286  difinfsn  7290  difinfinf  7291  djuinj  7296  0ct  7297  ctmlemr  7298  ctssdclemn0  7300  ctssdccl  7301  omct  7307  ctfoex  7308  finomni  7330  exmidomni  7332  fodjuomni  7339  ctssexmid  7340  fodjumkv  7350  nninfwlporlem  7363  nninfwlpoimlemg  7365  nninfwlpoim  7369  nninfinfwlpo  7370  card0  7383  ficardon  7384  exmidonfinlem  7394  dju1p1e2  7398  exmidfodomrlemim  7402  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  iftrueb01  7431  3nelsucpw1  7442  sucpw1nss3  7443  3nsssucpw1  7444  2onetap  7464  exmidmotap  7470  0npi  7523  dmaddpi  7535  dmmulpi  7536  1lt2pi  7550  0nnq  7574  1nq  7576  dmaddpq  7589  dmmulpq  7590  rec1nq  7605  1lt2nq  7616  halfnqq  7620  prarloclemarch2  7629  enq0enq  7641  nqnq0pi  7648  nnnq0lem1  7656  addnnnq0  7659  mulnnnq0  7660  nq0m0r  7666  addpinq1  7674  prarloclem5  7710  prarloclemcalc  7712  1pr  7764  1idprl  7800  1idpru  7801  ltexprlemm  7810  recexprlem1ssl  7843  recexprlem1ssu  7844  suplocexprlemell  7923  suplocexprlem2b  7924  suplocexprlemmu  7928  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemub  7933  suplocexprlemlub  7934  prsrlem1  7952  addsrpr  7955  mulsrpr  7956  gt0srpr  7958  0nsr  7959  0r  7960  1sr  7961  m1r  7962  m1m1sr  7971  caucvgsr  8012  suplocsrlempr  8017  addresr  8047  mulresr  8048  pitonnlem1  8055  peano1nnnn  8062  axi2m1  8085  axcnre  8091  peano5nnnn  8102  axcaucvg  8110  mpomulf  8159  mulridi  8171  mullidi  8172  pnfnre  8211  mnfnre  8212  pnfnemnf  8224  mnfxr  8226  rexri  8227  ltnri  8262  ltleii  8272  00id  8310  addridi  8311  addlidi  8312  0cnALT  8359  negeqi  8363  negicn  8370  neg0  8415  renegcli  8431  negcli  8437  negidi  8438  negnegi  8439  subidi  8440  subid1i  8441  negne0bi  8442  negrebi  8443  mul02i  8559  mul01i  8560  mulm1i  8572  leidi  8655  gt0ne0ii  8657  inelr  8754  msqge0i  8787  gt0ap0ii  8798  1div1e1  8874  div1i  8910  eqnegi  8911  recclapi  8912  recidapi  8913  divmulapi  8936  rerecclapi  8947  redivclapi  8949  rerecapb  9013  recgt0  9020  ltp1i  9075  divgt0ii  9089  ltmul1ii  9098  ltdiv1ii  9099  sup3exmid  9127  peano5nni  9136  nnrei  9142  1nn  9144  nngt0i  9163  neg1ap0  9242  2timesi  9263  times2i  9264  2nn  9295  3nn  9296  4nn  9297  5nn  9298  6nn  9299  7nn  9300  8nn  9301  9nn  9302  2muline0  9359  rehalfcli  9383  nn0ssre  9396  nnnn0i  9400  dfn2  9405  0nn0  9407  nn0ge0i  9419  zrei  9475  neg1z  9501  nn0negzi  9504  dfz2  9542  nneoi  9574  peano5uzi  9579  dfuzi  9580  nn0ind-raph  9587  deceq1i  9607  deceq2i  9608  10nn  9616  numltc  9626  eluzel2  9750  eluz1i  9753  nn0uz  9781  nnuz  9782  uzuzle35  9789  infrenegsupex  9818  lbzbi  9840  divfnzn  9845  qdivcl  9867  irrmul  9871  irrmulap  9872  cnref1o  9875  0ltpnf  10007  mnflt0  10009  0lepnf  10015  xrltnsym  10018  xrlttri3  10022  nltpnft  10039  ngtmnft  10042  xrrebnd  10044  xnegmnf  10054  xneg0  10056  xltnegi  10060  xaddmnf1  10073  xaddmnf2  10074  mnfaddpnf  10076  xaddid1  10087  xnn0lenn0nn0  10090  xnn0xadd0  10092  xposdif  10107  ixxex  10124  iooval2  10140  unirnioo  10198  ioorebasg  10200  elrege0  10201  fzval2  10236  fzen  10268  fzprval  10307  fztpval  10308  uzdisj  10318  ige2m1fz  10335  fz01or  10336  fz1ssfz0  10342  fz0sn  10346  fz0tp  10347  fz0to3un2pr  10348  fz0to4untppr  10349  nn0disj  10363  1fv  10364  4fvwrd4  10365  fzo0ss1  10401  fzo01  10451  fzo12sn  10452  fzo0to2pr  10453  fzo0to3tp  10454  fzo0to42pr  10455  zsupssdc  10488  qbtwnxr  10507  flval  10522  fldiv4lem1div2  10557  modqfrac  10589  modqmulnn  10594  q2txmodxeq0  10636  frecuzrdgdom  10670  frecuzrdgfun  10672  frecuzrdgsuct  10676  frechashgf1o  10680  nnct  10687  xnn0nnen  10689  fxnn0nninf  10691  0tonninf  10692  1tonninf  10693  iseqvalcbv  10711  ser0f  10786  0exp0e1  10796  qexpcl  10807  qexpclz  10812  m1expcl2  10813  1exp  10820  sqvali  10871  sqcli  10872  sqeq0i  10873  resqcli  10876  sq1  10885  neg1sqe1  10886  iexpcyc  10896  qsqeqor  10902  facnn  10979  fac0  10980  fac1  10981  fac2  10983  fac3  10984  fac4  10985  bcval  11001  bcm1k  11012  bcpasc  11018  bccl  11019  4bc3eq4  11025  4bc2eq6  11026  hashinfom  11030  hashennn  11032  hashfz1  11035  fihasheq0  11045  hash0  11048  hashsng  11050  fihashen1  11051  en1hash  11052  omgadd  11055  hashp1i  11064  hashxp  11080  fimaxq  11081  zfz1iso  11095  hash2en  11097  wrdexi  11116  wrdv  11119  wrdeqi  11126  wrd0  11128  lsw0  11151  ccatclab  11161  ccatidid  11177  s1prc  11190  ccat1st1st  11208  swrds1  11239  fnpfx  11248  swrdccatin2  11300  pfxccatin12lem2  11302  cats1fvn  11335  shftidt2  11383  cjexp  11444  re0  11446  im0  11447  re1  11448  im1  11449  cj0  11452  cji  11453  recli  11462  imcli  11463  cjcli  11464  replimi  11465  cjcji  11466  reim0bi  11467  rerebi  11468  cjrebi  11469  recji  11470  imcji  11471  cjmulrcli  11472  cjmulvali  11473  cjmulge0i  11474  renegi  11475  imnegi  11476  cjnegi  11477  addcji  11478  uzin2  11538  rexanuz  11539  rexfiuz  11540  sqrtrval  11551  sqrt0  11555  resqrexlemcalc3  11567  resqrexlemcvg  11570  resqrex  11577  abs0  11609  absi  11610  qabsor  11626  absimle  11635  recan  11660  caubnd2  11668  leabsi  11679  absrei  11680  sqrtpclii  11681  sqrtgt0ii  11682  absvalsqi  11691  absvalsq2i  11692  abscli  11693  absge0i  11694  absval2i  11695  abs00i  11696  absgt0api  11697  absnegi  11698  abscji  11699  releabsi  11700  infxrnegsupex  11814  xrbdtri  11827  cbvsum  11911  sumeq1i  11914  sum0  11939  isumz  11940  fisumss  11943  fsumsersdc  11946  fsumadd  11957  isumclim  11972  isumclim3  11974  fsumcnv  11988  modfsummodlem1  12007  fsumrelem  12022  binomlem  12034  binom  12035  arisum2  12050  expcnv  12055  0.999...  12072  prodf1f  12094  cbvprod  12109  prodeq1i  12112  zproddc  12130  zprodap0  12132  prod0  12136  fprodssdc  12141  prodsnf  12143  fprodcnv  12176  fprodge0  12188  fprodge1  12190  ef0lem  12211  esum  12213  ere  12221  ege2le3  12222  ef0  12223  eff2  12231  efsep  12242  reeff1  12251  sin0  12280  cos0  12281  ef01bndlem  12307  cos2bnd  12311  sincos1sgn  12316  sincos2sgn  12317  sin4lt0  12318  eirr  12330  0dvds  12362  dvds1  12404  z0even  12462  n2dvdsm1  12464  z2even  12465  n2dvds3  12466  ndvdssub  12481  ndvdsi  12484  flodddiv4  12487  bits0  12499  bitsfzo  12506  0bits  12510  m1bits  12511  bitsinv1lem  12512  bitsinv1  12513  gcddvds  12524  gcd1  12548  6gcd4e2  12556  bezoutlembi  12566  dfgcd3  12571  dfgcd2  12575  nninfctlemfo  12601  nninfct  12602  3lcm2e6woprm  12648  qredeu  12659  isprm2lem  12678  isprm3  12680  prm2orodd  12688  isprm5lem  12703  sqrt2irr0  12726  pw2dvds  12728  phicl2  12776  phi1  12781  dfphi2  12782  phiprmpw  12784  eulerthlemrprm  12791  eulerthlemh  12793  odzval  12804  oddprm  12822  pczpre  12860  pcdiv  12865  pc0  12867  pcqdiv  12870  pcrec  12871  pcexp  12872  pcxcl  12874  pcxqcl  12875  pcdvdstr  12890  pc2dvds  12893  dvdsprmpweqnn  12899  pcmpt  12906  qexpz  12915  pockthi  12921  1arith2  12931  4sqlemffi  12959  4sqlem11  12964  4sqlem13m  12966  4sqlem19  12972  dec2dvds  12974  dec5nprm  12977  modxai  12979  modxp1i  12981  numexp0  12985  numexp1  12986  ennnfonelemp1  13017  ennnfonelem1  13018  ennnfonelemkh  13023  ennnfonelemex  13025  ennnfonelemnn0  13033  ennnfonelemr  13034  exmidunben  13037  ctinfomlemom  13038  ctinfom  13039  ctinf  13041  qnnen  13042  omctfn  13054  omiunct  13055  ssnnctlemct  13057  nninfdc  13064  structcnvcnv  13088  structfun  13090  structfn  13091  ndxarg  13095  ndxid  13096  setsresg  13110  setsslnid  13124  basmex  13132  basmexd  13133  strleun  13177  strle1g  13179  prdsex  13342  prdsvallem  13345  prdsval  13346  prdsbaslemss  13347  imasaddfnlemg  13387  quslem  13397  xpsfrnel  13417  xpsff1o  13422  ismgmn0  13431  fn0g  13448  0g0  13449  fngsum  13461  idghm  13836  rhmfn  14176  rmodislmodlem  14354  rmodislmod  14355  lidlmex  14479  mopnset  14556  cntopex  14558  cnfldex  14563  cnfldbas  14564  mpocnfldadd  14565  mpocnfldmul  14567  cnfldcj  14569  cnfldtset  14570  cnfldle  14571  cnfldds  14572  cnring  14574  cnfld0  14575  cnfld1  14576  cnfldneg  14577  cnfldplusf  14578  cnfldsub  14579  cnfldmulg  14580  cnfldexp  14581  cnsubglem  14583  cnsubrglem  14584  gzsubrg  14586  gsumfzfsumlem0  14590  cnfldui  14593  zringring  14597  zringabl  14598  zringgrp  14599  zring1  14605  zringsubgval  14609  expghmap  14611  znval  14640  znle  14641  znbaslemnn  14643  znbas  14648  znzrh2  14650  znzrhval  14651  znzrhfo  14652  znleval  14657  znidom  14661  znidomb  14662  fnpsr  14671  psrelbas  14679  psradd  14683  psraddcl  14684  psr1clfi  14692  mplrcl  14698  mplbasss  14700  mpladd  14708  istopon  14727  topontopi  14730  toponunii  14731  toponrestid  14735  istps  14746  topontopn  14751  eltpsi  14755  eltg4i  14769  eltg3  14771  tg1  14773  tg2  14774  tgclb  14779  topnex  14800  sn0topon  14802  distps  14805  cldrcl  14816  sn0cld  14851  restco  14888  lmrcl  14906  ssidcn  14924  cnconst2  14947  cnptopresti  14952  cnptoprest  14953  txuni2  14970  txbas  14972  eltx  14973  txcnp  14985  upxp  14986  txcnmpt  14987  uptx  14988  txcn  14989  txrest  14990  txlm  14993  cnmptid  14995  cnmpt1st  15002  cnmpt2nd  15003  hmeofn  15016  psmetge0  15045  ismeti  15060  xmetunirn  15072  xmetge0  15079  unirnblps  15136  unirnbl  15137  mopnex  15219  qtopbasss  15235  retop  15238  uniretop  15239  iooretopg  15242  cnxmet  15245  cntoptopon  15246  cnbl0  15248  cnfldxms  15251  cnfldtps  15252  rexmet  15263  blssioo  15267  tgioo  15268  tgqioo  15269  cnopnap  15325  hovercncf  15360  limcresi  15380  dvfvalap  15395  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvcnp2cntop  15413  dvcoapbr  15421  dvexp2  15426  dvrecap  15427  dveflem  15440  dvef  15441  plyun0  15450  plyrecj  15477  dvply2  15481  reeff1o  15487  sin0pilem1  15495  sin0pilem2  15496  pilem3  15497  pigt2lt4  15498  pire  15500  sinhalfpilem  15505  pidiv2halves  15509  cosneghalfpi  15512  cospi  15514  efipi  15515  sin2pi  15517  cos2pi  15518  ef2pi  15519  cosq14gt0  15546  coseq00topi  15549  coseq0negpitopi  15550  sincos4thpi  15554  sincos6thpi  15556  sincos3rdpi  15557  pigt3  15558  cos02pilt1  15565  ioocosf1o  15568  dfrelog  15574  relogf1o  15575  relogcl  15576  relogiso  15587  rpcxpsqrt  15636  rpabscxpbnd  15654  2logb9irr  15685  2logb9irrALT  15688  sqrt2cxp2logb9e3  15689  2irrexpq  15690  2logb9irrap  15691  2irrexpqap  15692  mpodvdsmulf1o  15704  fsumdvdsmul  15705  perfectlem2  15714  lgsdir2lem1  15747  lgsdir2lem2  15748  lgsdir2lem4  15750  lgsdir2lem5  15751  lgsdi  15756  gausslemma2dlem0i  15776  gausslemma2dlem4  15783  lgseisenlem4  15792  lgsquadlem1  15796  lgsquad2lem2  15801  lgsquad2  15802  m1lgs  15804  2lgs2  15821  2lgslem4  15822  2lgsoddprmlem2  15825  2lgsoddprmlem3c  15828  2lgsoddprmlem3d  15829  2sqlem9  15843  2sqlem10  15844  1vgrex  15861  vtxval0  15894  iedgval0  15895  uhgr0  15926  upgrfi  15943  umgrislfupgrdom  15970  ausgrusgrben  16007  uspgredgiedg  16017  uspgriedgedg  16018  usgrislfuspgrdom  16029  uspgredg2vlem  16059  uspgredg2v  16060  usgr0  16078  griedg0prc  16089  0wlk0  16168  clwwlkn1  16213  clwwlkn2  16216  ex-fl  16257  ex-ceil  16258  ex-exp  16259  ex-fac  16260  ex-gcd  16263  bj-stfal  16274  bj-stst  16277  bj-dcfal  16287  bj-dcdc  16291  bj-stdc  16292  bj-dcst  16293  bj-el2oss1o  16306  elabf2  16314  bd0  16355  bdeli  16377  bdcriota  16414  bdbm1.3ii  16422  bdinex1  16430  bdssexi  16434  bj-inex  16438  bj-snex  16444  bj-sucex  16454  bj-d0clsepcl  16456  bj-omind  16465  bj-om  16468  bj-2inf  16469  bj-peano2  16470  bdpeano5  16474  bj-omssonALT  16494  bj-inf2vnlem1  16501  bj-omex2  16508  bj-nn0sucALT  16509  3dom  16523  012of  16528  2o01f  16529  subctctexmid  16537  pw1dceq  16541  nninfall  16547  nninfsellemqall  16553  nninfsellemeqinf  16554  nninfomnilem  16556  nninfomni  16557  exmidsbthrlem  16562  sbthom  16566  isomninnlem  16570  isomninn  16571  cvgcmp2nlemabs  16572  iooreen  16575  trilpolemisumle  16578  trilpolemeq1  16580  trilpo  16583  trirec0  16584  apdifflemr  16587  iswomninnlem  16589  iswomninn  16590  ismkvnnlem  16592  ismkvnn  16593  redcwlpo  16595  dcapnconst  16601  nconstwlpolem0  16603  nconstwlpo  16606  neapmkv  16608  neap0mkv  16609  taupi  16613