Theorem simpr 109

Description: Elimination of a conjunct. Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)

Assertion

Ref	Expression
simpr	|- ( ( ph /\ ps ) -> ps )

Proof of Theorem simpr

Step	Hyp	Ref	Expression
1		ax-ia2 106	1 |- ( ( ph /\ ps ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-ia2 106

This theorem is referenced by:  simpri  112  simprd  113  imp  123  adantld  276  ibar  299  pm3.42  330  pm3.4  331  anim12  341  simpl2im  383  sylancom  416  adantll  467  adantrl  469  adantlll  471  adantlrl  473  adantrll  475  adantrrl  477  simpllr  523  simplrr  525  simprlr  527  simprrr  529  anabs7  563  jcab  592  pm4.38  594  pm5.21  684  ioran  741  pm3.14  742  ordi  805  pm4.39  811  pm5.16  813  pm5.54dc  903  intnan  914  intnand  916  dcan  918  bimsc1  947  niabn  951  simp1r  1006  simp2r  1008  simp3r  1010  3anandirs  1326  bilukdc  1374  19.26  1457  exsimpr  1597  19.40  1610  cbvexh  1728  sbequilem  1810  spsbe  1814  cbvexdh  1896  euan  2053  moan  2066  datisi  2107  fresison  2115  rexex  2477  r19.26  2556  r19.29an  2572  r19.40  2583  cbvraldva2  2656  cbvrexdva2  2657  gencbvex  2727  rspct  2777  rspcimdv  2785  rspcimedv  2786  rr19.28v  2819  elrab3t  2834  reu6  2868  rmob  2996  csbiebt  3034  rabssab  3179  ssddif  3305  difin  3308  difrab  3345  dcun  3468  eqifdc  3501  ifmdc  3504  preqsn  3697  opprc2  3723  dfnfc2  3749  intmin4  3794  sndisj  3920  undifexmid  4112  exmid01  4116  pwntru  4117  exmidn0m  4119  exmidsssn  4120  exmidsssnc  4121  exmidundif  4124  exmidundifim  4125  exss  4144  euotd  4171  frirrg  4267  suctr  4338  abnexg  4362  ordtri2or2exmid  4481  wetriext  4486  reg3exmidlemwe  4488  tfisi  4496  peano2  4504  omsinds  4530  nnpredcl  4531  relop  4684  releldm  4769  relelrn  4770  resiexg  4859  trin2  4925  xpmlem  4954  unielrel  5061  relcoi2  5064  iota2df  5107  iota2  5109  funopab4  5155  fun11uni  5188  imadiflem  5197  imain  5200  fneq12  5211  f1ssr  5330  fvelrnb  5462  ssimaex  5475  fvmpt2d  5500  fvmptdf  5501  dffo3  5560  ffvresb  5576  fmptco  5579  funfvima3  5644  f1imass  5668  fliftf  5693  fliftval  5694  riota2df  5743  riota5f  5747  acexmidlemcase  5762  ovprc2  5801  eloprabga  5851  eqfnov2  5871  ovmpodxf  5889  ofvalg  5984  offval2  5990  ofrfval2  5991  caofinvl  5997  2ndrn  6074  1st2ndbr  6075  cnvf1o  6115  f1o2ndf1  6118  mpoxopoveq  6130  dftpos4  6153  tpostpos  6154  tposf12  6159  dfsmo2  6177  smores  6182  tfrlem1  6198  tfrlem3ag  6199  tfrlem3a  6200  tfrlemisucaccv  6215  tfrlemi1  6222  tfrexlem  6224  tfr1onlem3ag  6227  tfr1onlemsucaccv  6231  tfr1onlembxssdm  6233  tfr1onlembfn  6234  tfr1onlemaccex  6238  tfr1onlemres  6239  tfri1dALT  6241  tfrcllemsucaccv  6244  tfrcllembxssdm  6246  tfrcllembfn  6247  tfrcllemaccex  6251  tfrcllemres  6252  tfrcl  6254  rdgivallem  6271  rdgon  6276  frecabex  6288  frecabcl  6289  frectfr  6290  frecrdg  6298  oawordi  6358  nntri3  6386  nntr2  6392  dcdifsnid  6393  nnaordi  6397  nnaordex  6416  nnawordex  6417  nnm00  6418  ersymb  6436  ertr  6437  erref  6442  iserd  6448  swoer  6450  erth  6466  iinerm  6494  erinxp  6496  ecinxp  6497  qsel  6499  qliftel  6502  qliftfun  6504  fvdiagfn  6580  ixpssmapg  6615  resixp  6620  mptelixpg  6621  dom3  6663  ssdomg  6665  cnven  6695  xpen  6732  xpmapenlem  6736  ssenen  6738  phplem4dom  6749  phpm  6752  phpelm  6753  fidifsnen  6757  fin0  6772  fin0or  6773  isinfinf  6784  tridc  6786  fimax2gtrilemstep  6787  fimax2gtri  6788  finexdc  6789  en2eqpr  6794  fientri3  6796  unsnfidcex  6801  unsnfidcel  6802  unfidisj  6803  undifdcss  6804  undifdc  6805  unfiin  6807  fiintim  6810  fnfi  6818  relcnvfi  6822  f1dmvrnfibi  6825  iunfidisj  6827  f1finf1o  6828  fidcenumlemrks  6834  fidcenumlemr  6836  fidcenum  6837  fival  6851  elfi2  6853  ssfii  6855  fiss  6858  suplubti  6880  suplub2ti  6881  supelti  6882  supisolem  6888  supisoex  6889  infglbti  6905  ordiso2  6913  djuss  6948  updjudhcoinlf  6958  updjudhcoinrg  6959  updjud  6960  djudom  6971  omp1eomlem  6972  difinfsnlem  6977  difinfsn  6978  difinfinf  6979  ctm  6987  ctssdclemn0  6988  ctssdccl  6989  ctssdc  6991  enumctlemm  6992  enumct  6993  enomnilem  7003  finomni  7005  exmidomni  7007  fodjuomnilemdc  7009  fodjuomnilemres  7013  nnnninf  7016  ctssexmid  7017  ismkvnex  7022  mkvprop  7025  fodjumkvlemres  7026  en2eleq  7044  en2other2  7045  exmidfodomrlemeldju  7048  exmidfodomrlemreseldju  7049  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  exmidaclem  7057  dju1en  7062  djudomr  7069  dmaddpqlem  7178  nqpi  7179  mulcanenq  7186  ltaddnq  7208  ltexnqq  7209  prarloclemarch2  7220  ltrnqg  7221  ltnnnq  7224  enq0sym  7233  nqnq0pi  7239  nq0nn  7243  mulcanenq0ec  7246  addnq0mo  7248  mulnq0mo  7249  addnnnq0  7250  prloc  7292  prarloclemlt  7294  prarloclemlo  7295  ltdfpr  7307  genplt2i  7311  genpml  7318  genpmu  7319  addnqprllem  7328  addnqprulem  7329  addnqprl  7330  addnqpru  7331  nqprloc  7346  appdivnq  7364  appdiv0nq  7365  mulnqprl  7369  mulnqpru  7370  distrlem1prl  7383  distrlem1pru  7384  ltprordil  7390  1idprl  7391  1idpru  7392  ltexprlemrl  7411  ltexprlemru  7413  ltexpri  7414  addcanprleml  7415  addcanprlemu  7416  recexprlem1ssl  7434  recexpr  7439  aptiprlemu  7441  archpr  7444  cauappcvgprlemopl  7447  cauappcvgprlemdisj  7452  cauappcvgprlemloc  7453  cauappcvgprlemladdfu  7455  cauappcvgprlemladdfl  7456  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  caucvgprlemm  7469  caucvgprlemopl  7470  caucvgprlemloc  7476  caucvgprlemladdfu  7478  caucvgprlemladdrl  7479  caucvgprlemlim  7482  caucvgprprlemval  7489  caucvgprprlemml  7495  caucvgprprlemopl  7498  caucvgprprlemopu  7500  caucvgprprlemloc  7504  caucvgprprlemexbt  7507  caucvgprprlemexb  7508  caucvgprprlemaddq  7509  caucvgprprlemlim  7512  suplocexprlemru  7520  suplocexprlemloc  7522  suplocexprlemub  7524  suplocexprlemlub  7525  addsrmo  7544  mulsrmo  7545  addsrpr  7546  mulsrpr  7547  0idsr  7568  1idsr  7569  recexsrlem  7575  addgt0sr  7576  srpospr  7584  prsradd  7587  prsrlt  7588  caucvgsrlemfv  7592  caucvgsrlemgt1  7596  caucvgsrlemoffval  7597  caucvgsrlemoffcau  7599  caucvgsrlemoffres  7601  mappsrprg  7605  map2psrprg  7606  suplocsrlemb  7607  suplocsrlem  7609  suplocsr  7610  rereceu  7690  axarch  7692  nntopi  7695  axcaucvglemval  7698  axpre-suploclemres  7702  axpre-suploc  7703  axsuploc  7830  muladd11r  7911  cnegexlem1  7930  cnegex  7933  negeu  7946  pncan  7961  pncan3  7963  npcan  7964  addid0  8128  negf1o  8137  mulneg1  8150  lelttrdi  8181  ltnegcon2  8219  add20  8229  subge0  8230  lesub0  8234  reapval  8331  recexre  8333  apreap  8342  ltmul1a  8346  reapneg  8352  cru  8357  apsym  8361  apcotr  8362  apadd1  8363  apneg  8366  mulext1  8367  apti  8377  gt0ap0  8381  ap0gt0  8395  subap0  8398  lt0ap0  8403  recexap  8407  divmulassap  8448  divmulasscomap  8449  rerecclap  8483  recgt0  8601  prodgt0gt0  8602  lemul1a  8609  lemul12a  8613  lt2msq  8637  ltrec1  8639  recreclt  8651  negiso  8706  sup3exmid  8708  creui  8711  cju  8712  avglt2  8952  un0addcl  9003  nn0ge2m1nn  9030  nn0nndivcl  9032  elnn0z  9060  peano2z  9083  elz2  9115  suprzclex  9142  peano5uzti  9152  zindd  9162  btwnapz  9174  eluzadd  9347  nn0pzuz  9375  supinfneg  9383  infsupneg  9384  eluz2b2  9390  eqreznegel  9399  nn0ge2m1nnALT  9403  divfnzn  9406  qmulz  9408  qapne  9424  qreccl  9427  cnref1o  9433  ge0p1rp  9466  mul2lt0rlt0  9539  mul2lt0rgt0  9540  xrltso  9575  npnflt  9591  nmnfgt  9594  z2ge  9602  xltnegi  9611  xaddval  9621  xaddcom  9637  xnegdi  9644  xaddass  9645  xpncan  9647  xleadd1a  9649  xltadd1  9652  xlt2add  9656  xsubge0  9657  xposdif  9658  xlesubadd  9659  xleaddadd  9663  ixxssixx  9678  lincmb01cmp  9779  iccf1o  9780  zltaddlt1le  9782  fztri3or  9812  fzdcel  9813  fznlem  9814  fzn  9815  uzsubsubfz  9820  fzsplit2  9823  fzopth  9834  fzdifsuc  9854  fzrev2i  9859  elfz1b  9863  fzneuz  9874  fzrevral  9878  ige2m1fz  9883  elfz0ubfz0  9895  elfz0fzfz0  9896  4fvwrd4  9910  2ffzeq  9911  fzospliti  9946  fzosplit  9947  fzo1fzo0n0  9953  fzonmapblen  9957  fzoaddel  9962  fzosubel  9964  fzosubel3  9966  elfzodifsumelfzo  9971  elfzom1elp1fzo  9972  elfzom1p1elfzo  9984  elfzonelfzo  10000  peano2fzor  10002  exfzdc  10010  fvinim0ffz  10011  qtri3or  10013  exbtwnzlemstep  10018  rebtwn2zlemstep  10023  qbtwnxr  10028  apbtwnz  10040  flqge  10048  flqltnz  10053  flqaddz  10063  btwnzge0  10066  flltdivnn0lt  10070  intfracq  10086  flqdiv  10087  modqid0  10116  q0mod  10121  q1mod  10122  modqmuladdim  10133  modqmuladdnn0  10134  q2txmodxeq0  10150  q2submod  10151  modifeq2int  10152  modqsubdir  10159  modsumfzodifsn  10162  addmodlteq  10164  frec2uzzd  10166  frec2uzuzd  10168  frec2uzrand  10171  frec2uzf1od  10172  frecuzrdgrrn  10174  frec2uzrdg  10175  frecuzrdgtcl  10178  frecuzrdgsuc  10180  frecuzrdgg  10182  frecuzrdgdomlem  10183  frecuzrdgfunlem  10185  frecuzrdgsuctlem  10189  frecfzennn  10192  uzsinds  10208  seq3val  10224  seqvalcd  10225  seq3clss  10233  seq3feq2  10236  seq3feq  10238  ser3mono  10244  seq3split  10245  iseqf1olemkle  10250  iseqf1olemklt  10251  iseqf1olemqcl  10252  iseqf1olemnab  10254  iseqf1olemab  10255  iseqf1olemqf  10257  iseqf1olemmo  10258  iseqf1olemqf1o  10259  iseqf1olemqk  10260  iseqf1olemjpcl  10261  iseqf1olemqpcl  10262  iseqf1olemfvp  10263  seq3f1olemqsumkj  10264  seq3f1olemqsumk  10265  seq3f1olemqsum  10266  seq3f1oleml  10269  seq3f1o  10270  seq3id3  10273  seq3id  10274  seq3homo  10276  seq3z  10277  seqfeq3  10278  fser0const  10282  ser3ge0  10283  exp3vallem  10287  exp3val  10288  expnnval  10289  expp1  10293  rpexpcl  10305  expaddzaplem  10329  leexp1a  10341  exple1  10342  subsq  10392  binom2  10396  binom3  10402  bernneq3  10407  expnbnd  10408  expcan  10456  nn0opthd  10461  faclbnd  10480  faclbnd6  10483  facubnd  10484  facavg  10485  bcval  10488  bccmpl  10493  bcval5  10502  bcpasc  10505  hashennnuni  10518  hashennn  10519  hashfiv01gt1  10521  fihasheqf1oi  10527  hashnncl  10535  fseq1hash  10540  fiprsshashgt1  10556  fimaxq  10566  fnfz0hash  10568  ffzo0hash  10570  zfz1isolemiso  10575  zfz1iso  10577  seq3coll  10578  shftfvalg  10583  ovshftex  10584  shftdm  10587  shftfib  10588  shftval  10590  shftval5  10594  shftf  10595  2shfti  10596  seq3shft  10603  crre  10622  rereb  10628  cjreim2  10669  cjap  10671  caucvgrelemrec  10744  caucvgrelemcau  10745  caucvgre  10746  cvg1nlemf  10748  cvg1nlemres  10750  uzin2  10752  rexuz3  10755  recvguniq  10760  sqrt0  10769  resqrexlemdecn  10777  resqrexlemlo  10778  resqrexlemcalc3  10781  resqrexlemnm  10783  resqrexlemcvg  10784  resqrexlemoverl  10786  resqrexlemglsq  10787  resqrexlemga  10788  resqrex  10791  sqrtgt0  10799  absrpclap  10826  absext  10828  absmul  10834  leabs  10839  nn0abscl  10850  ltabs  10852  abslt  10853  absle  10854  abssubap0  10855  abstri  10869  cau3lem  10879  caubnd2  10882  maxabsle  10969  maxabslemlub  10972  maxabslemval  10973  maxcl  10975  maxleastb  10979  maxltsup  10983  rexanre  10985  rexico  10986  zmaxcl  10989  2zsupmax  10990  fimaxre2  10991  minmax  10994  min2inf  10997  minabs  11000  minclpr  11001  mul0inf  11005  xrmaxiflemcl  11007  xrmaxifle  11008  xrmaxiflemab  11009  xrmaxiflemlub  11010  xrmaxiflemcom  11011  xrmaxiflemval  11012  xrltmaxsup  11019  xrmaxltsup  11020  xrmaxaddlem  11022  xrmaxadd  11023  xrnegiso  11024  xrminmax  11027  xrbdtri  11038  clim  11043  climi2  11050  climconst2  11053  climuni  11055  climmpt  11062  climshftlemg  11064  climres  11065  climcn1  11070  subcn2  11073  cn1lem  11076  climadd  11088  climmul  11089  climsub  11090  climle  11096  climsqz  11097  climsqz2  11098  clim2ser  11099  clim2ser2  11100  iserex  11101  isermulc2  11102  iserle  11104  iserge0  11105  climub  11106  climrecvg1n  11110  climcvg1nlem  11111  serf0  11114  sumeq2  11121  sumfct  11136  sumrbdclem  11138  fsum3cvg  11139  sumrbdc  11140  summodclem2a  11143  summodclem2  11144  summodc  11145  zsumdc  11146  isum  11147  fsum3  11149  sum0  11150  isumz  11151  fsumf1o  11152  isumss  11153  fisumss  11154  isumss2  11155  fsum3cvg2  11156  fsum3cvg3  11158  fsum3ser  11159  fsumcl2lem  11160  fsumcllem  11161  fsumadd  11168  fsumsplit  11169  sumsnf  11171  isumclim3  11185  isummulc2  11188  isumadd  11193  fsum2dlemstep  11196  fsum2d  11197  fisumcom2  11200  fsum0diaglem  11202  fsumrev  11205  fsumshft  11206  fisumrev2  11208  fsummulc2  11210  fsumconst  11216  modfsummod  11220  fsum00  11224  fsumabs  11227  telfsumo  11228  fsumparts  11232  fsumrelem  11233  iserabs  11237  cvgcmpub  11238  fsumiun  11239  binom1dif  11249  bcxmas  11251  isumshft  11252  isumlessdc  11258  divcnv  11259  trireciplem  11262  trirecip  11263  expcnvap0  11264  expcnvre  11265  expcnv  11266  explecnv  11267  geolim  11273  geolim2  11274  geo2sum  11276  geo2lim  11278  geoisum  11279  geoisumr  11280  geoisum1  11281  geoisum1c  11282  cvgratnnlemnexp  11286  cvgratnnlemseq  11288  cvgratz  11294  mertenslem2  11298  mertensabs  11299  clim2prod  11301  clim2divap  11302  prodfdivap  11309  prodeq2  11319  prodrbdclem  11333  fproddccvg  11334  prodrbdclem2  11335  eftvalcn  11352  ef0lem  11355  efcvgfsum  11362  ege2le3  11366  efcj  11368  efaddlem  11369  efadd  11370  eftlcvg  11382  eftlub  11385  efler  11394  eflegeo  11397  tanvalap  11404  tanclap  11405  tanval2ap  11409  tanval3ap  11410  tannegap  11424  sinadd  11432  cosadd  11433  eirrap  11473  dvdsval2  11485  dvdsdc  11490  moddvds  11491  zdvdsdc  11503  dvdscmul  11509  dvdsmulc  11510  dvdscmulr  11511  dvdsmulcr  11512  modmulconst  11514  dvdsadd  11525  dvdsadd2b  11529  dvdslelemd  11530  dvdsle  11531  dvdsabseq  11534  dvdseq  11535  divconjdvds  11536  dvds1  11540  fzo0dvdseq  11544  dvdsmod  11549  oddm1even  11561  mod2eq1n2dvds  11565  evennn02n  11568  evennn2n  11569  divalglemnn  11604  divalglemnqt  11606  divalglemeunn  11607  divalglemex  11608  divalglemeuneg  11609  divalg  11610  divalgmod  11613  modremain  11615  infssuzex  11631  gcdsupex  11635  gcdsupcl  11636  gcdval  11637  dvdslegcd  11642  gcdnncl  11645  gcdneg  11659  gcdaddm  11661  gcd1  11664  bezoutlemnewy  11673  bezoutlemmain  11675  bezoutlemex  11678  bezoutlemzz  11679  bezoutlemaz  11680  bezoutlembz  11681  bezoutlembi  11682  bezoutlemle  11685  bezoutlemsup  11686  gcdass  11692  gcdzeq  11699  dvdsmulgcd  11702  bezoutr1  11710  algrp1  11716  algcvga  11721  eucalgval2  11723  eucalgf  11725  eucalglt  11727  lcmval  11733  lcmledvds  11740  lcmneg  11744  lcmgcd  11748  lcmid  11750  coprmgcdb  11758  ncoprmgcdne1b  11759  mulgcddvds  11764  rpmulgcd2  11765  qredeq  11766  divgcdcoprm0  11771  divgcdcoprmex  11772  cncongr1  11773  cncongr2  11774  isprm2lem  11786  prmind2  11790  sqnprm  11805  isprm6  11814  prmdvdsexp  11815  prmfac1  11819  rpexp  11820  rpexp1i  11821  sqrt2irr  11829  pw2dvdslemn  11832  pw2dvdseulemle  11834  oddpwdclemxy  11836  oddpwdclemdc  11840  oddpwdc  11841  znege1  11845  sqrt2irraplemnn  11846  sqrt2irrap  11847  divnumden  11863  qden1elz  11872  phibndlem  11881  dfphi2  11885  phiprmpw  11887  crth  11889  phimullem  11890  oddennn  11894  evenennn  11895  ennnfonelemk  11902  ennnfonelemg  11905  ennnfonelemss  11912  ennnfoneleminc  11913  ennnfonelemkh  11914  ennnfonelemhf1o  11915  ennnfonelemex  11916  ennnfonelemhom  11917  ennnfonelemrnh  11918  ennnfonelemfun  11919  ennnfonelemf1  11920  ennnfonelemrn  11921  ennnfonelemdm  11922  ennnfonelemnn0  11924  exmidunben  11928  ctinfomlemom  11929  ctinfom  11930  ctinf  11932  ctiunctlemudc  11939  ctiunctlemf  11940  ctiunct  11942  unct  11943  isstruct2im  11958  isstruct2r  11959  setsvalg  11978  setsslid  11998  ressid2  12007  ressval2  12008  2strbasg  12049  2stropg  12050  2strop1g  12053  restval  12115  restid2  12118  eltg3i  12214  bastg  12219  topbas  12225  tgtop  12226  tgidm  12232  tgss2  12237  bastop2  12242  epttop  12248  iuncld  12273  clsss2  12287  isopn3i  12293  neiint  12303  neii2  12307  neissex  12323  restbasg  12326  tgrest  12327  resttopon  12329  ssrest  12340  restopn2  12341  lmfval  12350  cnpval  12356  lmcvg  12375  iscnp4  12376  cncnpi  12386  cnconst2  12391  cnrest  12393  cnrest2  12394  cnrest2r  12395  cnptopresti  12396  cnptoprest  12397  cnptoprest2  12398  lmss  12404  lmtopcnp  12408  txcnp  12429  upxp  12430  uptx  12432  txcn  12433  txlm  12437  cnmpt11  12441  cnmpt1t  12443  hmeores  12473  txswaphmeo  12479  psmetres2  12491  ismet2  12512  xmettri2  12519  xmetres2  12537  metres2  12539  blfvalps  12543  bldisj  12559  xblss2ps  12562  xblss2  12563  xblm  12575  blssps  12585  blss  12586  metss2lem  12655  metss2  12656  bdxmet  12659  bdbl  12661  metrest  12664  xmetxpbl  12666  xmettxlem  12667  xmettx  12668  metcnp3  12669  metcnp2  12671  metcnpi  12673  metcnpi2  12674  txmetcnp  12676  qtopbas  12680  tgioo  12704  addcncntoplem  12709  fsumcncntop  12714  rescncf  12726  cncfco  12736  cncfcncntop  12738  cncfmptid  12741  addccncf  12744  cdivcncfap  12745  negcncf  12746  mulcncflem  12748  mulcncf  12749  dedekindeulemuub  12753  dedekindeulemloc  12755  dedekindeulemlu  12757  dedekindeulemeu  12758  dedekindeu  12759  suplociccreex  12760  suplociccex  12761  dedekindicclemuub  12762  dedekindicclemloc  12764  dedekindicclemlu  12766  dedekindicclemeu  12767  dedekindicclemicc  12768  ivthinclemlopn  12772  ivthinclemlr  12773  ivthinclemuopn  12774  ivthinclemur  12775  ivthinclemloc  12777  ivthinc  12779  limccl  12786  ellimc3apf  12787  limcdifap  12789  limcmpted  12790  limcimolemlt  12791  limcimo  12792  cnplimcim  12794  cnplimclemle  12795  cnplimclemr  12796  cnlimcim  12798  limccnpcntop  12802  limccoap  12805  reldvg  12806  dvfvalap  12808  dvfgg  12815  dvidlemap  12818  dvcnp2cntop  12821  dvcjbr  12830  dvcj  12831  dvfre  12832  dvexp  12833  dvrecap  12835  dveflem  12844  dvef  12845  sin0pilem1  12851  sin0pilem2  12852  pilem3  12853  ptolemy  12894  coseq0q4123  12904  coseq0negpitopi  12906  cos02pilt1  12921  bj-nnan  12937  bj-indind  13119  bj-omtrans  13143  pwtrufal  13181  pwle2  13182  pwf1oexmid  13183  subctctexmid  13185  nnsf  13188  peano4nninf  13189  nninfalllemn  13191  nninfalllem1  13192  nninfall  13193  nninfself  13198  nninfsellemeq  13199  nninfsellemqall  13200  nninfsellemeqinf  13201  nninfsel  13202  nninfomnilem  13203  nninffeq  13205  sbthom  13210  qdencn  13211  refeq  13212  isomninnlem  13214  trilpolemclim  13218  trilpolemcl  13219  trilpolemisumle  13220  trilpolemeq1  13222  trilpolemlt1  13223  trilpolemres  13224  taupi  13228