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  2790  elv  2803  elexi  2812  ceqsal  2829  vtocl3  2857  vtoclef  2876  vtocle  2877  spcv  2897  spcev  2898  clel3  2938  elabf  2946  elab2  2951  elab3  2955  euxfrdc  2989  reueq  3002  rmoimi2  3006  sbsbc  3032  sbc8g  3036  sbc6  3054  sbcie  3063  sbcrex  3108  csbvarg  3152  csbief  3169  csbie2  3174  sbnfc2  3185  sseli  3220  sselii  3221  sseq1i  3250  sseq2i  3251  difeq1i  3318  difeq2i  3319  uneq1i  3354  uneq2i  3355  ineq1i  3401  ineq2i  3402  ssinss1  3433  difdif2ss  3461  n0ii  3500  ne0ii  3501  vn0  3502  vn0m  3503  abf  3535  disj2  3547  difid  3560  0dif  3563  disjdif  3564  difin0  3565  undif1ss  3566  difdifdirss  3576  iftruei  3608  iffalsei  3611  ifbieq2i  3626  ifbieq12i  3628  pweqi  3653  pwid  3664  sneqi  3678  elsn  3682  elpr  3687  elsn2  3700  ralsn  3709  rexsn  3710  eltp  3714  rabrsndc  3734  preq1i  3746  preq2i  3747  prid1  3772  snnz  3786  snm  3787  prnz  3790  prm  3791  tpnz  3793  snss  3803  snsssn  3839  opeq1i  3860  opeq2i  3861  unieqi  3898  unissi  3911  inteqi  3927  intmin2  3949  intab  3952  intsn  3958  iinconstm  3974  iuniin  3975  iinss1  3977  iunxdif2  4014  ssiinf  4015  iinss  4017  iinss2  4018  iinab  4027  iundif2ss  4031  iindif2m  4033  iinin2m  4034  iunxsn  4042  iunxprg  4046  iinpw  4056  invdisjrab  4077  sndisj  4079  disjxsn  4081  breqi  4089  breq1i  4090  breq2i  4091  brab1  4131  opabbii  4151  truni  4196  bm1.3ii  4205  a9evsep  4206  ax9vsep  4207  zfnuleu  4208  axnul  4209  ssexi  4222  rabex  4228  rabex2  4230  elpw2  4241  pwnss  4243  iin0r  4253  intv  4254  pwex  4267  snex  4269  notnotsnex  4271  ord3ex  4274  dtruarb  4275  undifexmid  4277  intid  4310  opnzi  4321  copsexg  4330  opwo0id  4335  opelopabf  4363  epelc  4382  elon  4465  inton  4484  onn0  4491  onm  4492  elsuc  4497  elsuc2  4498  sucid  4508  iunsuc  4511  onordi  4517  ontrci  4518  onelssi  4520  eusvnf  4544  ssonunii  4581  sucex  4591  onssi  4607  onsuci  4608  ordtriexmidlem  4611  ordtriexmidlem2  4612  ordtriexmid  4613  ontriexmidim  4614  ordtri2orexmid  4615  2ordpr  4616  ontr2exmid  4617  onsucsssucexmid  4619  onsucelsucexmid  4622  regexmidlemm  4624  reg2exmid  4628  onirri  4635  ruALT  4643  onprc  4644  sucon  4645  dtru  4652  0elsucexmid  4657  ordpwsucexmid  4662  ordtri2or2exmid  4663  ontri2orexmidim  4664  dcextest  4673  omex  4685  find  4691  omelon  4701  nnoni  4703  limom  4706  nnregexmid  4713  omsinds  4714  xpeq1i  4739  xpeq2i  4740  0nelxp  4747  opthprc  4770  mosubop  4785  releqi  4802  relssi  4810  relin1  4837  relin2  4838  reldif  4839  inopab  4854  difopab  4855  xpiindim  4859  opabbi2dv  4871  ideq  4874  coeq1i  4881  coeq2i  4882  cnveqi  4897  eldm  4920  eldm2  4921  dmeqi  4924  dmv  4939  rneqi  4952  elrnmpti  4977  dmex  4991  rnex  4992  reseq1i  5001  reseq2i  5002  residm  5037  resex  5046  resmpt3  5054  imaeq1i  5065  imaeq2i  5066  elima  5073  imaex  5083  elimasn  5095  args  5097  epini  5099  dfse2  5101  eliniseg2  5108  relbrcnv  5109  cotr  5110  issref  5111  cnvsym  5112  asymref  5114  intirr  5115  codir  5117  qfto  5118  ssrnres  5171  cnveq0  5185  cnvsn0  5197  dmsnop  5202  rnsnop  5209  resdm2  5219  dfco2a  5229  cocnvcnv1  5239  coi2  5245  coires1  5246  cnvssrndm  5250  cossxp  5251  cocnvres  5253  relrelss  5255  relcoi2  5259  unidmrn  5261  dfdm2  5263  unixpm  5264  cnvexg  5266  cnvex  5267  cnviinm  5270  iotaval  5290  funeqi  5339  funi  5350  funres  5359  funcnvsn  5366  funcnvcnv  5380  funin  5392  funcnvres  5394  isarep2  5408  fneq1i  5415  fneq2i  5416  fndmi  5421  fnresdisj  5433  fnresi  5441  mpt0  5451  dmmpti  5453  feq1i  5466  feq2i  5467  fdmi  5481  fun2  5500  fssres  5503  resasplitss  5507  fintm  5513  fconst6  5527  f1ores  5589  foimacnv  5592  resdif  5596  funcocnv2  5599  f10d  5609  f1ovi  5614  fveq1i  5630  fveq2i  5632  0fv  5667  fvun1  5702  fvopab3ig  5710  fvmptss2  5711  mptrcl  5719  elfvmptrab1  5731  fndmdif  5742  fneqeql2  5746  f1oresrab  5802  fmptco  5803  funopsn  5819  fnressn  5829  fressnfv  5830  fmptap  5833  fvsnun1  5840  fvsnun2  5841  fsnunfv  5844  fconst2  5860  mptex  5869  fnfvimad  5879  riotabiia  5979  acexmidlema  5998  acexmidlemb  5999  acexmidlemcase  6002  acexmidlem2  6004  acexmidlemv  6005  oveq1i  6017  oveq2i  6018  oveqi  6020  oprabidlem  6038  0neqopab  6055  oprabbii  6065  oprabss  6096  mpompt  6102  funoprab  6110  fnoprab  6113  ovigg  6131  elmpocl  6206  relmptopab  6213  resfunexgALT  6259  cofunexg  6260  mptexw  6264  opabex3d  6272  opabex3  6273  1st0  6296  2nd0  6297  op1st  6298  op2nd  6299  f1stres  6311  f2ndres  6312  fo1stresm  6313  fo2ndresm  6314  1stcof  6315  2ndcof  6316  1stexg  6319  2ndexg  6320  releldm2  6337  reldm  6338  dfoprab3  6343  mpomptsx  6349  mpompts  6350  fnmpoi  6355  dmmpo  6356  mpoexxg  6362  mpoexw  6365  1stconst  6373  2ndconst  6374  dfmpo  6375  algrflem  6381  algrflemg  6382  cnvoprab  6386  f1od2  6387  mpoxopn0yelv  6391  mpoxopoveq  6392  tposssxp  6401  brtpos2  6403  reldmtpos  6405  dftpos2  6413  dftpos4  6415  tpostpos  6416  tpostpos2  6417  tposfo  6423  tposf  6424  tposeqi  6429  tposex  6430  tposoprab  6432  issmo  6440  smores  6444  smores2  6446  iordsmo  6449  smo0  6450  tfrlem8  6470  tfrexlem  6486  tfr1onlem3  6490  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlemres  6501  tfri1dALT  6503  tfri2  6518  rdgisuc1  6536  rdg0  6539  frecfun  6547  frec0g  6549  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecrdg  6560  2on0  6578  xp01disj  6587  2oconcl  6593  fnoa  6601  oaexg  6602  fnom  6604  omexg  6605  fnoei  6606  oeiexg  6607  oei0  6613  oacl  6614  oasuc  6618  o1p1e2  6622  omsuc  6626  nna0r  6632  nnm0r  6633  1onn  6674  2onn  6675  3onn  6676  4onn  6677  2ssom  6678  eqerlem  6719  eceq2i  6726  elqs  6741  qsex  6747  ecqs  6752  iinerm  6762  th3qlem1  6792  th3q  6795  mapsn  6845  mapsnf1o3  6852  ixpiinm  6879  ixpssmap  6887  brdom  6907  f1dom  6919  enref  6924  dom2  6934  idssen  6936  ssdomg  6938  ensymi  6942  ensn1  6956  fiprc  6976  1domsn  6984  dom1o  6985  xpcomf1o  6992  xpcomco  6993  dom0  7007  0dom  7008  xpmapenlem  7018  phplem2  7022  php5  7027  snnen2og  7028  1nen2  7030  php5dom  7032  ssfilem  7045  ssfiexmid  7046  domfiexmid  7048  0fi  7054  diffitest  7057  findcard  7058  findcard2  7059  findcard2s  7060  isinfinf  7067  ac6sfi  7068  inffiexmid  7079  pw1fin  7083  unfiexmid  7091  xpfi  7105  fisseneq  7107  ssfirab  7109  residfi  7118  en1eqsn  7126  snexxph  7128  sbthlem2  7136  sbthlemi3  7137  sbthlemi6  7140  sbthlem7  7141  fi0  7153  supeq1i  7166  infeq1i  7191  djuexb  7222  djuf1olemr  7232  inresflem  7238  djuinr  7241  updjudhcoinlf  7258  updjudhcoinrg  7259  casefun  7263  caserel  7265  caseinj  7267  caseinl  7269  caseinr  7270  omp1eomlem  7272  endjusym  7274  difinfsn  7278  difinfinf  7279  djuinj  7284  0ct  7285  ctmlemr  7286  ctssdclemn0  7288  ctssdccl  7289  omct  7295  ctfoex  7296  finomni  7318  exmidomni  7320  fodjuomni  7327  ctssexmid  7328  fodjumkv  7338  nninfwlporlem  7351  nninfwlpoimlemg  7353  nninfwlpoim  7357  nninfinfwlpo  7358  card0  7371  ficardon  7372  exmidonfinlem  7382  dju1p1e2  7386  exmidfodomrlemim  7390  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  iftrueb01  7419  3nelsucpw1  7430  sucpw1nss3  7431  3nsssucpw1  7432  2onetap  7452  exmidmotap  7458  0npi  7511  dmaddpi  7523  dmmulpi  7524  1lt2pi  7538  0nnq  7562  1nq  7564  dmaddpq  7577  dmmulpq  7578  rec1nq  7593  1lt2nq  7604  halfnqq  7608  prarloclemarch2  7617  enq0enq  7629  nqnq0pi  7636  nnnq0lem1  7644  addnnnq0  7647  mulnnnq0  7648  nq0m0r  7654  addpinq1  7662  prarloclem5  7698  prarloclemcalc  7700  1pr  7752  1idprl  7788  1idpru  7789  ltexprlemm  7798  recexprlem1ssl  7831  recexprlem1ssu  7832  suplocexprlemell  7911  suplocexprlem2b  7912  suplocexprlemmu  7916  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemub  7921  suplocexprlemlub  7922  prsrlem1  7940  addsrpr  7943  mulsrpr  7944  gt0srpr  7946  0nsr  7947  0r  7948  1sr  7949  m1r  7950  m1m1sr  7959  caucvgsr  8000  suplocsrlempr  8005  addresr  8035  mulresr  8036  pitonnlem1  8043  peano1nnnn  8050  axi2m1  8073  axcnre  8079  peano5nnnn  8090  axcaucvg  8098  mpomulf  8147  mulridi  8159  mullidi  8160  pnfnre  8199  mnfnre  8200  pnfnemnf  8212  mnfxr  8214  rexri  8215  ltnri  8250  ltleii  8260  00id  8298  addridi  8299  addlidi  8300  0cnALT  8347  negeqi  8351  negicn  8358  neg0  8403  renegcli  8419  negcli  8425  negidi  8426  negnegi  8427  subidi  8428  subid1i  8429  negne0bi  8430  negrebi  8431  mul02i  8547  mul01i  8548  mulm1i  8560  leidi  8643  gt0ne0ii  8645  inelr  8742  msqge0i  8775  gt0ap0ii  8786  1div1e1  8862  div1i  8898  eqnegi  8899  recclapi  8900  recidapi  8901  divmulapi  8924  rerecclapi  8935  redivclapi  8937  rerecapb  9001  recgt0  9008  ltp1i  9063  divgt0ii  9077  ltmul1ii  9086  ltdiv1ii  9087  sup3exmid  9115  peano5nni  9124  nnrei  9130  1nn  9132  nngt0i  9151  neg1ap0  9230  2timesi  9251  times2i  9252  2nn  9283  3nn  9284  4nn  9285  5nn  9286  6nn  9287  7nn  9288  8nn  9289  9nn  9290  2muline0  9347  rehalfcli  9371  nn0ssre  9384  nnnn0i  9388  dfn2  9393  0nn0  9395  nn0ge0i  9407  zrei  9463  neg1z  9489  nn0negzi  9492  dfz2  9530  nneoi  9562  peano5uzi  9567  dfuzi  9568  nn0ind-raph  9575  deceq1i  9595  deceq2i  9596  10nn  9604  numltc  9614  eluzel2  9738  eluz1i  9741  nn0uz  9769  nnuz  9770  infrenegsupex  9801  lbzbi  9823  divfnzn  9828  qdivcl  9850  irrmul  9854  irrmulap  9855  cnref1o  9858  0ltpnf  9990  mnflt0  9992  0lepnf  9998  xrltnsym  10001  xrlttri3  10005  nltpnft  10022  ngtmnft  10025  xrrebnd  10027  xnegmnf  10037  xneg0  10039  xltnegi  10043  xaddmnf1  10056  xaddmnf2  10057  mnfaddpnf  10059  xaddid1  10070  xnn0lenn0nn0  10073  xnn0xadd0  10075  xposdif  10090  ixxex  10107  iooval2  10123  unirnioo  10181  ioorebasg  10183  elrege0  10184  fzval2  10219  fzen  10251  fzprval  10290  fztpval  10291  uzdisj  10301  ige2m1fz  10318  fz01or  10319  fz1ssfz0  10325  fz0sn  10329  fz0tp  10330  fz0to3un2pr  10331  fz0to4untppr  10332  nn0disj  10346  1fv  10347  4fvwrd4  10348  fzo0ss1  10384  fzo01  10434  fzo12sn  10435  fzo0to2pr  10436  fzo0to3tp  10437  fzo0to42pr  10438  zsupssdc  10470  qbtwnxr  10489  flval  10504  fldiv4lem1div2  10539  modqfrac  10571  modqmulnn  10576  q2txmodxeq0  10618  frecuzrdgdom  10652  frecuzrdgfun  10654  frecuzrdgsuct  10658  frechashgf1o  10662  nnct  10669  xnn0nnen  10671  fxnn0nninf  10673  0tonninf  10674  1tonninf  10675  iseqvalcbv  10693  ser0f  10768  0exp0e1  10778  qexpcl  10789  qexpclz  10794  m1expcl2  10795  1exp  10802  sqvali  10853  sqcli  10854  sqeq0i  10855  resqcli  10858  sq1  10867  neg1sqe1  10868  iexpcyc  10878  qsqeqor  10884  facnn  10961  fac0  10962  fac1  10963  fac2  10965  fac3  10966  fac4  10967  bcval  10983  bcm1k  10994  bcpasc  11000  bccl  11001  4bc3eq4  11007  4bc2eq6  11008  hashinfom  11012  hashennn  11014  hashfz1  11017  fihasheq0  11027  hash0  11030  hashsng  11032  fihashen1  11033  omgadd  11036  hashp1i  11045  hashxp  11061  fimaxq  11062  zfz1iso  11076  hash2en  11078  wrdexi  11097  wrdv  11100  wrdeqi  11107  wrd0  11109  lsw0  11132  ccatclab  11142  ccatidid  11158  s1prc  11171  ccat1st1st  11187  swrds1  11215  fnpfx  11224  swrdccatin2  11276  pfxccatin12lem2  11278  cats1fvn  11311  shftidt2  11358  cjexp  11419  re0  11421  im0  11422  re1  11423  im1  11424  cj0  11427  cji  11428  recli  11437  imcli  11438  cjcli  11439  replimi  11440  cjcji  11441  reim0bi  11442  rerebi  11443  cjrebi  11444  recji  11445  imcji  11446  cjmulrcli  11447  cjmulvali  11448  cjmulge0i  11449  renegi  11450  imnegi  11451  cjnegi  11452  addcji  11453  uzin2  11513  rexanuz  11514  rexfiuz  11515  sqrtrval  11526  sqrt0  11530  resqrexlemcalc3  11542  resqrexlemcvg  11545  resqrex  11552  abs0  11584  absi  11585  qabsor  11601  absimle  11610  recan  11635  caubnd2  11643  leabsi  11654  absrei  11655  sqrtpclii  11656  sqrtgt0ii  11657  absvalsqi  11666  absvalsq2i  11667  abscli  11668  absge0i  11669  absval2i  11670  abs00i  11671  absgt0api  11672  absnegi  11673  abscji  11674  releabsi  11675  infxrnegsupex  11789  xrbdtri  11802  cbvsum  11886  sumeq1i  11889  sum0  11914  isumz  11915  fisumss  11918  fsumsersdc  11921  fsumadd  11932  isumclim  11947  isumclim3  11949  fsumcnv  11963  modfsummodlem1  11982  fsumrelem  11997  binomlem  12009  binom  12010  arisum2  12025  expcnv  12030  0.999...  12047  prodf1f  12069  cbvprod  12084  prodeq1i  12087  zproddc  12105  zprodap0  12107  prod0  12111  fprodssdc  12116  prodsnf  12118  fprodcnv  12151  fprodge0  12163  fprodge1  12165  ef0lem  12186  esum  12188  ere  12196  ege2le3  12197  ef0  12198  eff2  12206  efsep  12217  reeff1  12226  sin0  12255  cos0  12256  ef01bndlem  12282  cos2bnd  12286  sincos1sgn  12291  sincos2sgn  12292  sin4lt0  12293  eirr  12305  0dvds  12337  dvds1  12379  z0even  12437  n2dvdsm1  12439  z2even  12440  n2dvds3  12441  ndvdssub  12456  ndvdsi  12459  flodddiv4  12462  bits0  12474  bitsfzo  12481  0bits  12485  m1bits  12486  bitsinv1lem  12487  bitsinv1  12488  gcddvds  12499  gcd1  12523  6gcd4e2  12531  bezoutlembi  12541  dfgcd3  12546  dfgcd2  12550  nninfctlemfo  12576  nninfct  12577  3lcm2e6woprm  12623  qredeu  12634  isprm2lem  12653  isprm3  12655  prm2orodd  12663  isprm5lem  12678  sqrt2irr0  12701  pw2dvds  12703  phicl2  12751  phi1  12756  dfphi2  12757  phiprmpw  12759  eulerthlemrprm  12766  eulerthlemh  12768  odzval  12779  oddprm  12797  pczpre  12835  pcdiv  12840  pc0  12842  pcqdiv  12845  pcrec  12846  pcexp  12847  pcxcl  12849  pcxqcl  12850  pcdvdstr  12865  pc2dvds  12868  dvdsprmpweqnn  12874  pcmpt  12881  qexpz  12890  pockthi  12896  1arith2  12906  4sqlemffi  12934  4sqlem11  12939  4sqlem13m  12941  4sqlem19  12947  dec2dvds  12949  dec5nprm  12952  modxai  12954  modxp1i  12956  numexp0  12960  numexp1  12961  ennnfonelemp1  12992  ennnfonelem1  12993  ennnfonelemkh  12998  ennnfonelemex  13000  ennnfonelemnn0  13008  ennnfonelemr  13009  exmidunben  13012  ctinfomlemom  13013  ctinfom  13014  ctinf  13016  qnnen  13017  omctfn  13029  omiunct  13030  ssnnctlemct  13032  nninfdc  13039  structcnvcnv  13063  structfun  13065  structfn  13066  ndxarg  13070  ndxid  13071  setsresg  13085  setsslnid  13099  basmex  13107  basmexd  13108  strleun  13152  strle1g  13154  prdsex  13317  prdsvallem  13320  prdsval  13321  prdsbaslemss  13322  imasaddfnlemg  13362  quslem  13372  xpsfrnel  13392  xpsff1o  13397  ismgmn0  13406  fn0g  13423  0g0  13424  fngsum  13436  idghm  13811  rhmfn  14151  rmodislmodlem  14329  rmodislmod  14330  lidlmex  14454  mopnset  14531  cntopex  14533  cnfldex  14538  cnfldbas  14539  mpocnfldadd  14540  mpocnfldmul  14542  cnfldcj  14544  cnfldtset  14545  cnfldle  14546  cnfldds  14547  cnring  14549  cnfld0  14550  cnfld1  14551  cnfldneg  14552  cnfldplusf  14553  cnfldsub  14554  cnfldmulg  14555  cnfldexp  14556  cnsubglem  14558  cnsubrglem  14559  gzsubrg  14561  gsumfzfsumlem0  14565  cnfldui  14568  zringring  14572  zringabl  14573  zringgrp  14574  zring1  14580  zringsubgval  14584  expghmap  14586  znval  14615  znle  14616  znbaslemnn  14618  znbas  14623  znzrh2  14625  znzrhval  14626  znzrhfo  14627  znleval  14632  znidom  14636  znidomb  14637  fnpsr  14646  psrelbas  14654  psradd  14658  psraddcl  14659  psr1clfi  14667  mplrcl  14673  mplbasss  14675  mpladd  14683  istopon  14702  topontopi  14705  toponunii  14706  toponrestid  14710  istps  14721  topontopn  14726  eltpsi  14730  eltg4i  14744  eltg3  14746  tg1  14748  tg2  14749  tgclb  14754  topnex  14775  sn0topon  14777  distps  14780  cldrcl  14791  sn0cld  14826  restco  14863  lmrcl  14881  ssidcn  14899  cnconst2  14922  cnptopresti  14927  cnptoprest  14928  txuni2  14945  txbas  14947  eltx  14948  txcnp  14960  upxp  14961  txcnmpt  14962  uptx  14963  txcn  14964  txrest  14965  txlm  14968  cnmptid  14970  cnmpt1st  14977  cnmpt2nd  14978  hmeofn  14991  psmetge0  15020  ismeti  15035  xmetunirn  15047  xmetge0  15054  unirnblps  15111  unirnbl  15112  mopnex  15194  qtopbasss  15210  retop  15213  uniretop  15214  iooretopg  15217  cnxmet  15220  cntoptopon  15221  cnbl0  15223  cnfldxms  15226  cnfldtps  15227  rexmet  15238  blssioo  15242  tgioo  15243  tgqioo  15244  cnopnap  15300  hovercncf  15335  limcresi  15355  dvfvalap  15370  dvidlemap  15380  dvidrelem  15381  dvidsslem  15382  dvcnp2cntop  15388  dvcoapbr  15396  dvexp2  15401  dvrecap  15402  dveflem  15415  dvef  15416  plyun0  15425  plyrecj  15452  dvply2  15456  reeff1o  15462  sin0pilem1  15470  sin0pilem2  15471  pilem3  15472  pigt2lt4  15473  pire  15475  sinhalfpilem  15480  pidiv2halves  15484  cosneghalfpi  15487  cospi  15489  efipi  15490  sin2pi  15492  cos2pi  15493  ef2pi  15494  cosq14gt0  15521  coseq00topi  15524  coseq0negpitopi  15525  sincos4thpi  15529  sincos6thpi  15531  sincos3rdpi  15532  pigt3  15533  cos02pilt1  15540  ioocosf1o  15543  dfrelog  15549  relogf1o  15550  relogcl  15551  relogiso  15562  rpcxpsqrt  15611  rpabscxpbnd  15629  2logb9irr  15660  2logb9irrALT  15663  sqrt2cxp2logb9e3  15664  2irrexpq  15665  2logb9irrap  15666  2irrexpqap  15667  mpodvdsmulf1o  15679  fsumdvdsmul  15680  perfectlem2  15689  lgsdir2lem1  15722  lgsdir2lem2  15723  lgsdir2lem4  15725  lgsdir2lem5  15726  lgsdi  15731  gausslemma2dlem0i  15751  gausslemma2dlem4  15758  lgseisenlem4  15767  lgsquadlem1  15771  lgsquad2lem2  15776  lgsquad2  15777  m1lgs  15779  2lgs2  15796  2lgslem4  15797  2lgsoddprmlem2  15800  2lgsoddprmlem3c  15803  2lgsoddprmlem3d  15804  2sqlem9  15818  2sqlem10  15819  1vgrex  15836  vtxval0  15869  iedgval0  15870  uhgr0  15900  upgrfi  15917  umgrislfupgrdom  15944  ausgrusgrben  15981  uspgredgiedg  15991  uspgriedgedg  15992  usgrislfuspgrdom  16003  uspgredg2vlem  16033  uspgredg2v  16034  0wlk0  16112  ex-fl  16144  ex-ceil  16145  ex-exp  16146  ex-fac  16147  ex-gcd  16150  bj-stfal  16161  bj-stst  16164  bj-dcfal  16174  bj-dcdc  16178  bj-stdc  16179  bj-dcst  16180  bj-el2oss1o  16193  elabf2  16201  bd0  16242  bdeli  16264  bdcriota  16301  bdbm1.3ii  16309  bdinex1  16317  bdssexi  16321  bj-inex  16325  bj-snex  16331  bj-sucex  16341  bj-d0clsepcl  16343  bj-omind  16352  bj-om  16355  bj-2inf  16356  bj-peano2  16357  bdpeano5  16361  bj-omssonALT  16381  bj-inf2vnlem1  16388  bj-omex2  16395  bj-nn0sucALT  16396  3dom  16411  012of  16416  2o01f  16417  subctctexmid  16425  pw1dceq  16429  nninfall  16435  nninfsellemqall  16441  nninfsellemeqinf  16442  nninfomnilem  16444  nninfomni  16445  exmidsbthrlem  16450  sbthom  16454  isomninnlem  16458  isomninn  16459  cvgcmp2nlemabs  16460  iooreen  16463  trilpolemisumle  16466  trilpolemeq1  16468  trilpo  16471  trirec0  16472  apdifflemr  16475  iswomninnlem  16477  iswomninn  16478  ismkvnnlem  16480  ismkvnn  16481  redcwlpo  16483  dcapnconst  16489  nconstwlpolem0  16491  nconstwlpo  16494  neapmkv  16496  neap0mkv  16497  taupi  16501