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 ph is true, and ph implies ps, then ps 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	|- ph
maj	|- ( ph -> ps )

Assertion

Ref	Expression
ax-mp	|- ps

Detailed syntax breakdown of Axiom ax-mp

Step	Hyp	Ref	Expression
1		wps	1 wff ps

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  703  ori  727  orci  735  olci  736  biorfi  750  imorri  753  dcbii  844  simp1i  1011  simp2i  1012  simp3i  1013  3mix1i  1174  3mix2i  1175  3mix3i  1176  3jaoi  1318  mptru  1384  dfnot  1393  mptnan  1445  mtpor  1447  mtpxor  1448  dcfromnotnotr  1470  dcfromcon  1471  dcfrompeirce  1472  mpg  1477  19.23h  1524  hbequid  1539  axi12  1540  nfri  1545  spi  1562  19.21  1609  eximii  1628  19.35i  1651  nfn  1684  19.37aiv  1701  19.23  1704  exan  1719  equid  1727  hbae  1744  equvini  1784  equveli  1785  sbid  1800  sbieh  1816  exdistrfor  1826  dveeq2or  1842  ax11v  1853  ax11ev  1854  equs5or  1856  sb4or  1859  sb4bor  1861  nfsb2or  1863  sbequilem  1864  sbequi  1865  speiv  1888  nfsbxy  1973  nfsbxyt  1974  sbco  1999  sbcocom  2001  sbcomxyyz  2003  sbal1yz  2032  dvelimALT  2041  dvelimfv  2042  dvelimor  2049  eumoi  2090  moani  2128  elsb1  2187  elsb2  2188  eqeq1i  2217  eqeq2i  2220  eleq1i  2275  eleq2i  2276  nfcrii  2345  neeq1i  2395  neeq2i  2396  necon3i  2428  rspec  2562  rgen2a  2564  mprg  2567  r19.21  2586  r19.23  2619  raleqi  2712  rexeqi  2713  rabeqif  2770  elv  2783  elexi  2792  ceqsal  2809  vtocl3  2837  vtoclef  2856  vtocle  2857  spcv  2877  spcev  2878  clel3  2918  elabf  2926  elab2  2931  elab3  2935  euxfrdc  2969  reueq  2982  rmoimi2  2986  sbsbc  3012  sbc8g  3016  sbc6  3034  sbcie  3043  sbcrex  3088  csbvarg  3132  csbief  3149  csbie2  3154  sbnfc2  3165  sseli  3200  sselii  3201  sseq1i  3230  sseq2i  3231  difeq1i  3298  difeq2i  3299  uneq1i  3334  uneq2i  3335  ineq1i  3381  ineq2i  3382  ssinss1  3413  difdif2ss  3441  n0ii  3480  ne0ii  3481  vn0  3482  vn0m  3483  abf  3515  disj2  3527  difid  3540  0dif  3543  disjdif  3544  difin0  3545  undif1ss  3546  difdifdirss  3556  iftruei  3588  iffalsei  3591  ifbieq2i  3606  ifbieq12i  3608  pweqi  3633  pwid  3644  sneqi  3658  elsn  3662  elpr  3667  elsn2  3680  ralsn  3689  rexsn  3690  eltp  3694  rabrsndc  3714  preq1i  3726  preq2i  3727  prid1  3752  snnz  3765  snm  3766  prnz  3769  prm  3770  tpnz  3772  snss  3782  snsssn  3818  opeq1i  3839  opeq2i  3840  unieqi  3877  unissi  3890  inteqi  3906  intmin2  3928  intab  3931  intsn  3937  iinconstm  3953  iuniin  3954  iinss1  3956  iunxdif2  3993  ssiinf  3994  iinss  3996  iinss2  3997  iinab  4006  iundif2ss  4010  iindif2m  4012  iinin2m  4013  iunxsn  4021  iunxprg  4025  iinpw  4035  invdisjrab  4056  sndisj  4058  disjxsn  4060  breqi  4068  breq1i  4069  breq2i  4070  brab1  4110  opabbii  4130  truni  4175  bm1.3ii  4184  a9evsep  4185  ax9vsep  4186  zfnuleu  4187  axnul  4188  ssexi  4201  rabex  4207  rabex2  4209  elpw2  4220  pwnss  4222  iin0r  4232  intv  4233  pwex  4246  snex  4248  notnotsnex  4250  ord3ex  4253  dtruarb  4254  undifexmid  4256  intid  4289  opnzi  4300  copsexg  4309  opwo0id  4314  opelopabf  4342  epelc  4359  elon  4442  inton  4461  onn0  4468  onm  4469  elsuc  4474  elsuc2  4475  sucid  4485  iunsuc  4488  onordi  4494  ontrci  4495  onelssi  4497  eusvnf  4521  ssonunii  4558  sucex  4568  onssi  4584  onsuci  4585  ordtriexmidlem  4588  ordtriexmidlem2  4589  ordtriexmid  4590  ontriexmidim  4591  ordtri2orexmid  4592  2ordpr  4593  ontr2exmid  4594  onsucsssucexmid  4596  onsucelsucexmid  4599  regexmidlemm  4601  reg2exmid  4605  onirri  4612  ruALT  4620  onprc  4621  sucon  4622  dtru  4629  0elsucexmid  4634  ordpwsucexmid  4639  ordtri2or2exmid  4640  ontri2orexmidim  4641  dcextest  4650  omex  4662  find  4668  omelon  4678  nnoni  4680  limom  4683  nnregexmid  4690  omsinds  4691  xpeq1i  4716  xpeq2i  4717  0nelxp  4724  opthprc  4747  mosubop  4762  releqi  4779  relssi  4787  relin1  4814  relin2  4815  reldif  4816  inopab  4831  difopab  4832  xpiindim  4836  opabbi2dv  4848  ideq  4851  coeq1i  4858  coeq2i  4859  cnveqi  4874  eldm  4897  eldm2  4898  dmeqi  4901  dmv  4916  rneqi  4928  elrnmpti  4953  dmex  4967  rnex  4968  reseq1i  4977  reseq2i  4978  residm  5013  resex  5022  resmpt3  5030  imaeq1i  5041  imaeq2i  5042  elima  5049  imaex  5059  elimasn  5071  args  5073  epini  5075  dfse2  5077  eliniseg2  5084  relbrcnv  5085  cotr  5086  issref  5087  cnvsym  5088  asymref  5090  intirr  5091  codir  5093  qfto  5094  ssrnres  5147  cnveq0  5161  cnvsn0  5173  dmsnop  5178  rnsnop  5185  resdm2  5195  dfco2a  5205  cocnvcnv1  5215  coi2  5221  coires1  5222  cnvssrndm  5226  cossxp  5227  cocnvres  5229  relrelss  5231  relcoi2  5235  unidmrn  5237  dfdm2  5239  unixpm  5240  cnvexg  5242  cnvex  5243  cnviinm  5246  iotaval  5266  funeqi  5315  funi  5326  funres  5335  funcnvsn  5342  funcnvcnv  5356  funin  5368  funcnvres  5370  isarep2  5384  fneq1i  5391  fneq2i  5392  fndmi  5397  fnresdisj  5409  fnresi  5417  mpt0  5427  dmmpti  5429  feq1i  5442  feq2i  5443  fdmi  5457  fun2  5474  fssres  5477  resasplitss  5481  fintm  5487  fconst6  5501  f1ores  5563  foimacnv  5566  resdif  5570  funcocnv2  5573  f10d  5583  f1ovi  5588  fveq1i  5604  fveq2i  5606  0fv  5639  fvun1  5673  fvopab3ig  5681  fvmptss2  5682  mptrcl  5690  elfvmptrab1  5702  fndmdif  5713  fneqeql2  5717  f1oresrab  5773  fmptco  5774  funopsn  5790  fnressn  5798  fressnfv  5799  fmptap  5802  fvsnun1  5809  fvsnun2  5810  fsnunfv  5813  fconst2  5829  mptex  5838  riotabiia  5946  acexmidlema  5965  acexmidlemb  5966  acexmidlemcase  5969  acexmidlem2  5971  acexmidlemv  5972  oveq1i  5984  oveq2i  5985  oveqi  5987  oprabidlem  6005  0neqopab  6020  oprabbii  6030  oprabss  6061  mpompt  6067  funoprab  6075  fnoprab  6078  ovigg  6096  elmpocl  6171  resfunexgALT  6223  cofunexg  6224  mptexw  6228  opabex3d  6236  opabex3  6237  1st0  6260  2nd0  6261  op1st  6262  op2nd  6263  f1stres  6275  f2ndres  6276  fo1stresm  6277  fo2ndresm  6278  1stcof  6279  2ndcof  6280  1stexg  6283  2ndexg  6284  releldm2  6301  reldm  6302  dfoprab3  6307  mpomptsx  6313  mpompts  6314  fnmpoi  6319  dmmpo  6320  mpoexxg  6326  mpoexw  6329  1stconst  6337  2ndconst  6338  dfmpo  6339  algrflem  6345  algrflemg  6346  cnvoprab  6350  f1od2  6351  mpoxopn0yelv  6355  mpoxopoveq  6356  tposssxp  6365  brtpos2  6367  reldmtpos  6369  dftpos2  6377  dftpos4  6379  tpostpos  6380  tpostpos2  6381  tposfo  6387  tposf  6388  tposeqi  6393  tposex  6394  tposoprab  6396  issmo  6404  smores  6408  smores2  6410  iordsmo  6413  smo0  6414  tfrlem8  6434  tfrexlem  6450  tfr1onlem3  6454  tfr1onlemsucaccv  6457  tfr1onlembxssdm  6459  tfr1onlemres  6465  tfri1dALT  6467  tfri2  6482  rdgisuc1  6500  rdg0  6503  frecfun  6511  frec0g  6513  freccllem  6518  frecfcllem  6520  frecsuclem  6522  frecrdg  6524  2on0  6542  xp01disj  6549  2oconcl  6555  fnoa  6563  oaexg  6564  fnom  6566  omexg  6567  fnoei  6568  oeiexg  6569  oei0  6575  oacl  6576  oasuc  6580  o1p1e2  6584  omsuc  6588  nna0r  6594  nnm0r  6595  1onn  6636  2onn  6637  3onn  6638  4onn  6639  2ssom  6640  eqerlem  6681  eceq2i  6688  elqs  6703  qsex  6709  ecqs  6714  iinerm  6724  th3qlem1  6754  th3q  6757  mapsn  6807  mapsnf1o3  6814  ixpiinm  6841  ixpssmap  6849  brdom  6869  f1dom  6881  enref  6886  dom2  6896  idssen  6898  ssdomg  6900  ensymi  6904  ensn1  6918  fiprc  6938  1domsn  6946  xpcomf1o  6952  xpcomco  6953  dom0  6967  0dom  6968  xpmapenlem  6978  phplem2  6982  php5  6987  snnen2og  6988  1nen2  6990  php5dom  6992  ssfilem  7005  ssfiexmid  7006  domfiexmid  7008  0fin  7014  diffitest  7017  findcard  7018  findcard2  7019  findcard2s  7020  isinfinf  7027  ac6sfi  7028  inffiexmid  7036  pw1fin  7040  unfiexmid  7048  xpfi  7062  fisseneq  7064  ssfirab  7066  residfi  7075  en1eqsn  7083  snexxph  7085  sbthlem2  7093  sbthlemi3  7094  sbthlemi6  7097  sbthlem7  7098  fi0  7110  supeq1i  7123  infeq1i  7148  djuexb  7179  djuf1olemr  7189  inresflem  7195  djuinr  7198  updjudhcoinlf  7215  updjudhcoinrg  7216  casefun  7220  caserel  7222  caseinj  7224  caseinl  7226  caseinr  7227  omp1eomlem  7229  endjusym  7231  difinfsn  7235  difinfinf  7236  djuinj  7241  0ct  7242  ctmlemr  7243  ctssdclemn0  7245  ctssdccl  7246  omct  7252  ctfoex  7253  finomni  7275  exmidomni  7277  fodjuomni  7284  ctssexmid  7285  fodjumkv  7295  nninfwlporlem  7308  nninfwlpoimlemg  7310  nninfwlpoim  7314  nninfinfwlpo  7315  card0  7328  ficardon  7329  exmidonfinlem  7339  dju1p1e2  7343  exmidfodomrlemim  7347  exmidfodomrlemr  7348  exmidfodomrlemrALT  7349  iftrueb01  7376  3nelsucpw1  7387  sucpw1nss3  7388  3nsssucpw1  7389  2onetap  7409  exmidmotap  7415  0npi  7468  dmaddpi  7480  dmmulpi  7481  1lt2pi  7495  0nnq  7519  1nq  7521  dmaddpq  7534  dmmulpq  7535  rec1nq  7550  1lt2nq  7561  halfnqq  7565  prarloclemarch2  7574  enq0enq  7586  nqnq0pi  7593  nnnq0lem1  7601  addnnnq0  7604  mulnnnq0  7605  nq0m0r  7611  addpinq1  7619  prarloclem5  7655  prarloclemcalc  7657  1pr  7709  1idprl  7745  1idpru  7746  ltexprlemm  7755  recexprlem1ssl  7788  recexprlem1ssu  7789  suplocexprlemell  7868  suplocexprlem2b  7869  suplocexprlemmu  7873  suplocexprlemdisj  7875  suplocexprlemloc  7876  suplocexprlemub  7878  suplocexprlemlub  7879  prsrlem1  7897  addsrpr  7900  mulsrpr  7901  gt0srpr  7903  0nsr  7904  0r  7905  1sr  7906  m1r  7907  m1m1sr  7916  caucvgsr  7957  suplocsrlempr  7962  addresr  7992  mulresr  7993  pitonnlem1  8000  peano1nnnn  8007  axi2m1  8030  axcnre  8036  peano5nnnn  8047  axcaucvg  8055  mpomulf  8104  mulridi  8116  mullidi  8117  pnfnre  8156  mnfnre  8157  pnfnemnf  8169  mnfxr  8171  rexri  8172  ltnri  8207  ltleii  8217  00id  8255  addridi  8256  addlidi  8257  0cnALT  8304  negeqi  8308  negicn  8315  neg0  8360  renegcli  8376  negcli  8382  negidi  8383  negnegi  8384  subidi  8385  subid1i  8386  negne0bi  8387  negrebi  8388  mul02i  8504  mul01i  8505  mulm1i  8517  leidi  8600  gt0ne0ii  8602  inelr  8699  msqge0i  8732  gt0ap0ii  8743  1div1e1  8819  div1i  8855  eqnegi  8856  recclapi  8857  recidapi  8858  divmulapi  8881  rerecclapi  8892  redivclapi  8894  rerecapb  8958  recgt0  8965  ltp1i  9020  divgt0ii  9034  ltmul1ii  9043  ltdiv1ii  9044  sup3exmid  9072  peano5nni  9081  nnrei  9087  1nn  9089  nngt0i  9108  neg1ap0  9187  2timesi  9208  times2i  9209  2nn  9240  3nn  9241  4nn  9242  5nn  9243  6nn  9244  7nn  9245  8nn  9246  9nn  9247  2muline0  9304  rehalfcli  9328  nn0ssre  9341  nnnn0i  9345  dfn2  9350  0nn0  9352  nn0ge0i  9364  zrei  9420  neg1z  9446  nn0negzi  9449  dfz2  9487  nneoi  9519  peano5uzi  9524  dfuzi  9525  nn0ind-raph  9532  deceq1i  9552  deceq2i  9553  10nn  9561  numltc  9571  eluzel2  9695  eluz1i  9697  nn0uz  9725  nnuz  9726  infrenegsupex  9757  lbzbi  9779  divfnzn  9784  qdivcl  9806  irrmul  9810  irrmulap  9811  cnref1o  9814  0ltpnf  9946  mnflt0  9948  0lepnf  9954  xrltnsym  9957  xrlttri3  9961  nltpnft  9978  ngtmnft  9981  xrrebnd  9983  xnegmnf  9993  xneg0  9995  xltnegi  9999  xaddmnf1  10012  xaddmnf2  10013  mnfaddpnf  10015  xaddid1  10026  xnn0lenn0nn0  10029  xnn0xadd0  10031  xposdif  10046  ixxex  10063  iooval2  10079  unirnioo  10137  ioorebasg  10139  elrege0  10140  fzval2  10175  fzen  10207  fzprval  10246  fztpval  10247  uzdisj  10257  ige2m1fz  10274  fz01or  10275  fz1ssfz0  10281  fz0sn  10285  fz0tp  10286  fz0to3un2pr  10287  fz0to4untppr  10288  nn0disj  10302  1fv  10303  4fvwrd4  10304  fzo0ss1  10340  fzo01  10389  fzo12sn  10390  fzo0to2pr  10391  fzo0to3tp  10392  fzo0to42pr  10393  zsupssdc  10425  qbtwnxr  10444  flval  10459  fldiv4lem1div2  10494  modqfrac  10526  modqmulnn  10531  q2txmodxeq0  10573  frecuzrdgdom  10607  frecuzrdgfun  10609  frecuzrdgsuct  10613  frechashgf1o  10617  nnct  10624  xnn0nnen  10626  fxnn0nninf  10628  0tonninf  10629  1tonninf  10630  iseqvalcbv  10648  ser0f  10723  0exp0e1  10733  qexpcl  10744  qexpclz  10749  m1expcl2  10750  1exp  10757  sqvali  10808  sqcli  10809  sqeq0i  10810  resqcli  10813  sq1  10822  neg1sqe1  10823  iexpcyc  10833  qsqeqor  10839  facnn  10916  fac0  10917  fac1  10918  fac2  10920  fac3  10921  fac4  10922  bcval  10938  bcm1k  10949  bcpasc  10955  bccl  10956  4bc3eq4  10962  4bc2eq6  10963  hashinfom  10967  hashennn  10969  hashfz1  10972  fihasheq0  10982  hash0  10985  hashsng  10987  fihashen1  10988  omgadd  10991  hashp1i  10999  hashxp  11015  fimaxq  11016  zfz1iso  11030  hash2en  11032  wrdexi  11051  wrdv  11054  wrdeqi  11061  wrd0  11063  lsw0  11085  ccatclab  11095  ccatidid  11111  s1prc  11122  ccat1st1st  11138  swrds1  11166  fnpfx  11175  swrdccatin2  11227  pfxccatin12lem2  11229  cats1fvn  11262  shftidt2  11309  cjexp  11370  re0  11372  im0  11373  re1  11374  im1  11375  cj0  11378  cji  11379  recli  11388  imcli  11389  cjcli  11390  replimi  11391  cjcji  11392  reim0bi  11393  rerebi  11394  cjrebi  11395  recji  11396  imcji  11397  cjmulrcli  11398  cjmulvali  11399  cjmulge0i  11400  renegi  11401  imnegi  11402  cjnegi  11403  addcji  11404  uzin2  11464  rexanuz  11465  rexfiuz  11466  sqrtrval  11477  sqrt0  11481  resqrexlemcalc3  11493  resqrexlemcvg  11496  resqrex  11503  abs0  11535  absi  11536  qabsor  11552  absimle  11561  recan  11586  caubnd2  11594  leabsi  11605  absrei  11606  sqrtpclii  11607  sqrtgt0ii  11608  absvalsqi  11617  absvalsq2i  11618  abscli  11619  absge0i  11620  absval2i  11621  abs00i  11622  absgt0api  11623  absnegi  11624  abscji  11625  releabsi  11626  infxrnegsupex  11740  xrbdtri  11753  cbvsum  11837  sumeq1i  11840  sum0  11865  isumz  11866  fisumss  11869  fsumsersdc  11872  fsumadd  11883  isumclim  11898  isumclim3  11900  fsumcnv  11914  modfsummodlem1  11933  fsumrelem  11948  binomlem  11960  binom  11961  arisum2  11976  expcnv  11981  0.999...  11998  prodf1f  12020  cbvprod  12035  prodeq1i  12038  zproddc  12056  zprodap0  12058  prod0  12062  fprodssdc  12067  prodsnf  12069  fprodcnv  12102  fprodge0  12114  fprodge1  12116  ef0lem  12137  esum  12139  ere  12147  ege2le3  12148  ef0  12149  eff2  12157  efsep  12168  reeff1  12177  sin0  12206  cos0  12207  ef01bndlem  12233  cos2bnd  12237  sincos1sgn  12242  sincos2sgn  12243  sin4lt0  12244  eirr  12256  0dvds  12288  dvds1  12330  z0even  12388  n2dvdsm1  12390  z2even  12391  n2dvds3  12392  ndvdssub  12407  ndvdsi  12410  flodddiv4  12413  bits0  12425  bitsfzo  12432  0bits  12436  m1bits  12437  bitsinv1lem  12438  bitsinv1  12439  gcddvds  12450  gcd1  12474  6gcd4e2  12482  bezoutlembi  12492  dfgcd3  12497  dfgcd2  12501  nninfctlemfo  12527  nninfct  12528  3lcm2e6woprm  12574  qredeu  12585  isprm2lem  12604  isprm3  12606  prm2orodd  12614  isprm5lem  12629  sqrt2irr0  12652  pw2dvds  12654  phicl2  12702  phi1  12707  dfphi2  12708  phiprmpw  12710  eulerthlemrprm  12717  eulerthlemh  12719  odzval  12730  oddprm  12748  pczpre  12786  pcdiv  12791  pc0  12793  pcqdiv  12796  pcrec  12797  pcexp  12798  pcxcl  12800  pcxqcl  12801  pcdvdstr  12816  pc2dvds  12819  dvdsprmpweqnn  12825  pcmpt  12832  qexpz  12841  pockthi  12847  1arith2  12857  4sqlemffi  12885  4sqlem11  12890  4sqlem13m  12892  4sqlem19  12898  dec2dvds  12900  dec5nprm  12903  modxai  12905  modxp1i  12907  numexp0  12911  numexp1  12912  ennnfonelemp1  12943  ennnfonelem1  12944  ennnfonelemkh  12949  ennnfonelemex  12951  ennnfonelemnn0  12959  ennnfonelemr  12960  exmidunben  12963  ctinfomlemom  12964  ctinfom  12965  ctinf  12967  qnnen  12968  omctfn  12980  omiunct  12981  ssnnctlemct  12983  nninfdc  12990  structcnvcnv  13014  structfun  13016  structfn  13017  ndxarg  13021  ndxid  13022  setsresg  13036  setsslnid  13050  basmex  13058  basmexd  13059  strleun  13103  strle1g  13105  prdsex  13268  prdsvallem  13271  prdsval  13272  prdsbaslemss  13273  imasaddfnlemg  13313  quslem  13323  xpsfrnel  13343  xpsff1o  13348  ismgmn0  13357  fn0g  13374  0g0  13375  fngsum  13387  idghm  13762  rhmfn  14101  rmodislmodlem  14279  rmodislmod  14280  lidlmex  14404  mopnset  14481  cntopex  14483  cnfldex  14488  cnfldbas  14489  mpocnfldadd  14490  mpocnfldmul  14492  cnfldcj  14494  cnfldtset  14495  cnfldle  14496  cnfldds  14497  cnring  14499  cnfld0  14500  cnfld1  14501  cnfldneg  14502  cnfldplusf  14503  cnfldsub  14504  cnfldmulg  14505  cnfldexp  14506  cnsubglem  14508  cnsubrglem  14509  gzsubrg  14511  gsumfzfsumlem0  14515  cnfldui  14518  zringring  14522  zringabl  14523  zringgrp  14524  zring1  14530  zringsubgval  14534  expghmap  14536  znval  14565  znle  14566  znbaslemnn  14568  znbas  14573  znzrh2  14575  znzrhval  14576  znzrhfo  14577  znleval  14582  znidom  14586  znidomb  14587  fnpsr  14596  psrelbas  14604  psradd  14608  psraddcl  14609  psr1clfi  14617  mplrcl  14623  mplbasss  14625  mpladd  14633  istopon  14652  topontopi  14655  toponunii  14656  toponrestid  14660  istps  14671  topontopn  14676  eltpsi  14680  eltg4i  14694  eltg3  14696  tg1  14698  tg2  14699  tgclb  14704  topnex  14725  sn0topon  14727  distps  14730  cldrcl  14741  sn0cld  14776  restco  14813  lmrcl  14830  ssidcn  14849  cnconst2  14872  cnptopresti  14877  cnptoprest  14878  txuni2  14895  txbas  14897  eltx  14898  txcnp  14910  upxp  14911  txcnmpt  14912  uptx  14913  txcn  14914  txrest  14915  txlm  14918  cnmptid  14920  cnmpt1st  14927  cnmpt2nd  14928  hmeofn  14941  psmetge0  14970  ismeti  14985  xmetunirn  14997  xmetge0  15004  unirnblps  15061  unirnbl  15062  mopnex  15144  qtopbasss  15160  retop  15163  uniretop  15164  iooretopg  15167  cnxmet  15170  cntoptopon  15171  cnbl0  15173  cnfldxms  15176  cnfldtps  15177  rexmet  15188  blssioo  15192  tgioo  15193  tgqioo  15194  cnopnap  15250  hovercncf  15285  limcresi  15305  dvfvalap  15320  dvidlemap  15330  dvidrelem  15331  dvidsslem  15332  dvcnp2cntop  15338  dvcoapbr  15346  dvexp2  15351  dvrecap  15352  dveflem  15365  dvef  15366  plyun0  15375  plyrecj  15402  dvply2  15406  reeff1o  15412  sin0pilem1  15420  sin0pilem2  15421  pilem3  15422  pigt2lt4  15423  pire  15425  sinhalfpilem  15430  pidiv2halves  15434  cosneghalfpi  15437  cospi  15439  efipi  15440  sin2pi  15442  cos2pi  15443  ef2pi  15444  cosq14gt0  15471  coseq00topi  15474  coseq0negpitopi  15475  sincos4thpi  15479  sincos6thpi  15481  sincos3rdpi  15482  pigt3  15483  cos02pilt1  15490  ioocosf1o  15493  dfrelog  15499  relogf1o  15500  relogcl  15501  relogiso  15512  rpcxpsqrt  15561  rpabscxpbnd  15579  2logb9irr  15610  2logb9irrALT  15613  sqrt2cxp2logb9e3  15614  2irrexpq  15615  2logb9irrap  15616  2irrexpqap  15617  mpodvdsmulf1o  15629  fsumdvdsmul  15630  perfectlem2  15639  lgsdir2lem1  15672  lgsdir2lem2  15673  lgsdir2lem4  15675  lgsdir2lem5  15676  lgsdi  15681  gausslemma2dlem0i  15701  gausslemma2dlem4  15708  lgseisenlem4  15717  lgsquadlem1  15721  lgsquad2lem2  15726  lgsquad2  15727  m1lgs  15729  2lgs2  15746  2lgslem4  15747  2lgsoddprmlem2  15750  2lgsoddprmlem3c  15753  2lgsoddprmlem3d  15754  2sqlem9  15768  2sqlem10  15769  1vgrex  15786  vtxval0  15819  iedgval0  15820  uhgr0  15850  upgrfi  15867  umgrislfupgrdom  15894  ausgrusgrben  15931  uspgredgiedg  15941  uspgriedgedg  15942  usgrislfuspgrdom  15953  uspgredg2vlem  15983  uspgredg2v  15984  ex-fl  15999  ex-ceil  16000  ex-exp  16001  ex-fac  16002  ex-gcd  16005  bj-stfal  16016  bj-stst  16019  bj-dcfal  16029  bj-dcdc  16033  bj-stdc  16034  bj-dcst  16035  bj-el2oss1o  16048  elabf2  16056  bd0  16097  bdeli  16119  bdcriota  16156  bdbm1.3ii  16164  bdinex1  16172  bdssexi  16176  bj-inex  16180  bj-snex  16186  bj-sucex  16196  bj-d0clsepcl  16198  bj-omind  16207  bj-om  16210  bj-2inf  16211  bj-peano2  16212  bdpeano5  16216  bj-omssonALT  16236  bj-inf2vnlem1  16243  bj-omex2  16250  bj-nn0sucALT  16251  dom1o  16266  012of  16268  2o01f  16269  subctctexmid  16277  nninfall  16286  nninfsellemqall  16292  nninfsellemeqinf  16293  nninfomnilem  16295  nninfomni  16296  exmidsbthrlem  16301  sbthom  16305  isomninnlem  16309  isomninn  16310  cvgcmp2nlemabs  16311  iooreen  16314  trilpolemisumle  16317  trilpolemeq1  16319  trilpo  16322  trirec0  16323  apdifflemr  16326  iswomninnlem  16328  iswomninn  16329  ismkvnnlem  16331  ismkvnn  16332  redcwlpo  16334  dcapnconst  16340  nconstwlpolem0  16342  nconstwlpo  16345  neapmkv  16347  neap0mkv  16348  taupi  16352