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	⊢ ((𝜑 ∧ 𝜓) → 𝜓)

Proof of Theorem simpr

Step	Hyp	Ref	Expression
1		ax-ia2 106	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)

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  1898  euan  2055  moan  2068  datisi  2109  fresison  2117  rexex  2479  r19.26  2558  r19.29an  2574  r19.40  2585  cbvraldva2  2661  cbvrexdva2  2662  gencbvex  2732  rspct  2782  rspcimdv  2790  rspcimedv  2791  rr19.28v  2824  elrab3t  2839  reu6  2873  rmob  3001  csbiebt  3039  rabssab  3184  ssddif  3310  difin  3313  difrab  3350  dcun  3473  eqifdc  3506  ifmdc  3509  preqsn  3702  opprc2  3728  dfnfc2  3754  intmin4  3799  sndisj  3925  undifexmid  4117  exmid01  4121  pwntru  4122  exmidn0m  4124  exmidsssn  4125  exmidsssnc  4126  exmidundif  4129  exmidundifim  4130  exss  4149  euotd  4176  frirrg  4272  suctr  4343  abnexg  4367  ordtri2or2exmid  4486  wetriext  4491  reg3exmidlemwe  4493  tfisi  4501  peano2  4509  omsinds  4535  nnpredcl  4536  relop  4689  releldm  4774  relelrn  4775  resiexg  4864  trin2  4930  xpmlem  4959  unielrel  5066  relcoi2  5069  iota2df  5112  iota2  5114  funopab4  5160  fun11uni  5193  imadiflem  5202  imain  5205  fneq12  5216  f1ssr  5335  fvelrnb  5469  ssimaex  5482  fvmpt2d  5507  fvmptdf  5508  dffo3  5567  ffvresb  5583  fmptco  5586  funfvima3  5651  f1imass  5675  fliftf  5700  fliftval  5701  riota2df  5750  riota5f  5754  acexmidlemcase  5769  ovprc2  5808  eloprabga  5858  eqfnov2  5878  ovmpodxf  5896  ofvalg  5991  offval2  5997  ofrfval2  5998  caofinvl  6004  2ndrn  6081  1st2ndbr  6082  cnvf1o  6122  f1o2ndf1  6125  mpoxopoveq  6137  dftpos4  6160  tpostpos  6161  tposf12  6166  dfsmo2  6184  smores  6189  tfrlem1  6205  tfrlem3ag  6206  tfrlem3a  6207  tfrlemisucaccv  6222  tfrlemi1  6229  tfrexlem  6231  tfr1onlem3ag  6234  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemaccex  6245  tfr1onlemres  6246  tfri1dALT  6248  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemaccex  6258  tfrcllemres  6259  tfrcl  6261  rdgivallem  6278  rdgon  6283  frecabex  6295  frecabcl  6296  frectfr  6297  frecrdg  6305  oawordi  6365  nntri3  6393  nntr2  6399  dcdifsnid  6400  nnaordi  6404  nnaordex  6423  nnawordex  6424  nnm00  6425  ersymb  6443  ertr  6444  erref  6449  iserd  6455  swoer  6457  erth  6473  iinerm  6501  erinxp  6503  ecinxp  6504  qsel  6506  qliftel  6509  qliftfun  6511  fvdiagfn  6587  ixpssmapg  6622  resixp  6627  mptelixpg  6628  dom3  6670  ssdomg  6672  cnven  6702  xpen  6739  xpmapenlem  6743  ssenen  6745  phplem4dom  6756  phpm  6759  phpelm  6760  fidifsnen  6764  fin0  6779  fin0or  6780  isinfinf  6791  tridc  6793  fimax2gtrilemstep  6794  fimax2gtri  6795  finexdc  6796  en2eqpr  6801  fientri3  6803  unsnfidcex  6808  unsnfidcel  6809  unfidisj  6810  undifdcss  6811  undifdc  6812  unfiin  6814  fiintim  6817  fnfi  6825  relcnvfi  6829  f1dmvrnfibi  6832  iunfidisj  6834  f1finf1o  6835  fidcenumlemrks  6841  fidcenumlemr  6843  fidcenum  6844  fival  6858  elfi2  6860  ssfii  6862  fiss  6865  suplubti  6887  suplub2ti  6888  supelti  6889  supisolem  6895  supisoex  6896  infglbti  6912  ordiso2  6920  djuss  6955  updjudhcoinlf  6965  updjudhcoinrg  6966  updjud  6967  djudom  6978  omp1eomlem  6979  difinfsnlem  6984  difinfsn  6985  difinfinf  6986  ctm  6994  ctssdclemn0  6995  ctssdccl  6996  ctssdc  6998  enumctlemm  6999  enumct  7000  enomnilem  7010  finomni  7012  exmidomni  7014  fodjuomnilemdc  7016  fodjuomnilemres  7020  nnnninf  7023  ctssexmid  7024  ismkvnex  7029  mkvprop  7032  fodjumkvlemres  7033  en2eleq  7051  en2other2  7052  exmidfodomrlemeldju  7055  exmidfodomrlemreseldju  7056  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  exmidaclem  7064  dju1en  7069  djudomr  7076  dmaddpqlem  7185  nqpi  7186  mulcanenq  7193  ltaddnq  7215  ltexnqq  7216  prarloclemarch2  7227  ltrnqg  7228  ltnnnq  7231  enq0sym  7240  nqnq0pi  7246  nq0nn  7250  mulcanenq0ec  7253  addnq0mo  7255  mulnq0mo  7256  addnnnq0  7257  prloc  7299  prarloclemlt  7301  prarloclemlo  7302  ltdfpr  7314  genplt2i  7318  genpml  7325  genpmu  7326  addnqprllem  7335  addnqprulem  7336  addnqprl  7337  addnqpru  7338  nqprloc  7353  appdivnq  7371  appdiv0nq  7372  mulnqprl  7376  mulnqpru  7377  distrlem1prl  7390  distrlem1pru  7391  ltprordil  7397  1idprl  7398  1idpru  7399  ltexprlemrl  7418  ltexprlemru  7420  ltexpri  7421  addcanprleml  7422  addcanprlemu  7423  recexprlem1ssl  7441  recexpr  7446  aptiprlemu  7448  archpr  7451  cauappcvgprlemopl  7454  cauappcvgprlemdisj  7459  cauappcvgprlemloc  7460  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemloc  7483  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  caucvgprlemlim  7489  caucvgprprlemval  7496  caucvgprprlemml  7502  caucvgprprlemopl  7505  caucvgprprlemopu  7507  caucvgprprlemloc  7511  caucvgprprlemexbt  7514  caucvgprprlemexb  7515  caucvgprprlemaddq  7516  caucvgprprlemlim  7519  suplocexprlemru  7527  suplocexprlemloc  7529  suplocexprlemub  7531  suplocexprlemlub  7532  addsrmo  7551  mulsrmo  7552  addsrpr  7553  mulsrpr  7554  0idsr  7575  1idsr  7576  recexsrlem  7582  addgt0sr  7583  srpospr  7591  prsradd  7594  prsrlt  7595  caucvgsrlemfv  7599  caucvgsrlemgt1  7603  caucvgsrlemoffval  7604  caucvgsrlemoffcau  7606  caucvgsrlemoffres  7608  mappsrprg  7612  map2psrprg  7613  suplocsrlemb  7614  suplocsrlem  7616  suplocsr  7617  rereceu  7697  axarch  7699  nntopi  7702  axcaucvglemval  7705  axpre-suploclemres  7709  axpre-suploc  7710  axsuploc  7837  muladd11r  7918  cnegexlem1  7937  cnegex  7940  negeu  7953  pncan  7968  pncan3  7970  npcan  7971  addid0  8135  negf1o  8144  mulneg1  8157  lelttrdi  8188  ltnegcon2  8226  add20  8236  subge0  8237  lesub0  8241  reapval  8338  recexre  8340  apreap  8349  ltmul1a  8353  reapneg  8359  cru  8364  apsym  8368  apcotr  8369  apadd1  8370  apneg  8373  mulext1  8374  apti  8384  gt0ap0  8388  ap0gt0  8402  subap0  8405  lt0ap0  8410  recexap  8414  divmulassap  8455  divmulasscomap  8456  rerecclap  8490  recgt0  8608  prodgt0gt0  8609  lemul1a  8616  lemul12a  8620  lt2msq  8644  ltrec1  8646  recreclt  8658  negiso  8713  sup3exmid  8715  creui  8718  cju  8719  avglt2  8959  un0addcl  9010  nn0ge2m1nn  9037  nn0nndivcl  9039  elnn0z  9067  peano2z  9090  elz2  9122  suprzclex  9149  peano5uzti  9159  zindd  9169  btwnapz  9181  eluzadd  9354  nn0pzuz  9382  supinfneg  9390  infsupneg  9391  eluz2b2  9397  eqreznegel  9406  nn0ge2m1nnALT  9410  divfnzn  9413  qmulz  9415  qapne  9431  qreccl  9434  cnref1o  9440  ge0p1rp  9473  mul2lt0rlt0  9546  mul2lt0rgt0  9547  xrltso  9582  npnflt  9598  nmnfgt  9601  z2ge  9609  xltnegi  9618  xaddval  9628  xaddcom  9644  xnegdi  9651  xaddass  9652  xpncan  9654  xleadd1a  9656  xltadd1  9659  xlt2add  9663  xsubge0  9664  xposdif  9665  xlesubadd  9666  xleaddadd  9670  ixxssixx  9685  lincmb01cmp  9786  iccf1o  9787  zltaddlt1le  9789  fztri3or  9819  fzdcel  9820  fznlem  9821  fzn  9822  uzsubsubfz  9827  fzsplit2  9830  fzopth  9841  fzdifsuc  9861  fzrev2i  9866  elfz1b  9870  fzneuz  9881  fzrevral  9885  ige2m1fz  9890  elfz0ubfz0  9902  elfz0fzfz0  9903  4fvwrd4  9917  2ffzeq  9918  fzospliti  9953  fzosplit  9954  fzo1fzo0n0  9960  fzonmapblen  9964  fzoaddel  9969  fzosubel  9971  fzosubel3  9973  elfzodifsumelfzo  9978  elfzom1elp1fzo  9979  elfzom1p1elfzo  9991  elfzonelfzo  10007  peano2fzor  10009  exfzdc  10017  fvinim0ffz  10018  qtri3or  10020  exbtwnzlemstep  10025  rebtwn2zlemstep  10030  qbtwnxr  10035  apbtwnz  10047  flqge  10055  flqltnz  10060  flqaddz  10070  btwnzge0  10073  flltdivnn0lt  10077  intfracq  10093  flqdiv  10094  modqid0  10123  q0mod  10128  q1mod  10129  modqmuladdim  10140  modqmuladdnn0  10141  q2txmodxeq0  10157  q2submod  10158  modifeq2int  10159  modqsubdir  10166  modsumfzodifsn  10169  addmodlteq  10171  frec2uzzd  10173  frec2uzuzd  10175  frec2uzrand  10178  frec2uzf1od  10179  frecuzrdgrrn  10181  frec2uzrdg  10182  frecuzrdgtcl  10185  frecuzrdgsuc  10187  frecuzrdgg  10189  frecuzrdgdomlem  10190  frecuzrdgfunlem  10192  frecuzrdgsuctlem  10196  frecfzennn  10199  uzsinds  10215  seq3val  10231  seqvalcd  10232  seq3clss  10240  seq3feq2  10243  seq3feq  10245  ser3mono  10251  seq3split  10252  iseqf1olemkle  10257  iseqf1olemklt  10258  iseqf1olemqcl  10259  iseqf1olemnab  10261  iseqf1olemab  10262  iseqf1olemqf  10264  iseqf1olemmo  10265  iseqf1olemqf1o  10266  iseqf1olemqk  10267  iseqf1olemjpcl  10268  iseqf1olemqpcl  10269  iseqf1olemfvp  10270  seq3f1olemqsumkj  10271  seq3f1olemqsumk  10272  seq3f1olemqsum  10273  seq3f1oleml  10276  seq3f1o  10277  seq3id3  10280  seq3id  10281  seq3homo  10283  seq3z  10284  seqfeq3  10285  fser0const  10289  ser3ge0  10290  exp3vallem  10294  exp3val  10295  expnnval  10296  expp1  10300  rpexpcl  10312  expaddzaplem  10336  leexp1a  10348  exple1  10349  subsq  10399  binom2  10403  binom3  10409  bernneq3  10414  expnbnd  10415  expcan  10463  nn0opthd  10468  faclbnd  10487  faclbnd6  10490  facubnd  10491  facavg  10492  bcval  10495  bccmpl  10500  bcval5  10509  bcpasc  10512  hashennnuni  10525  hashennn  10526  hashfiv01gt1  10528  fihasheqf1oi  10534  hashnncl  10542  fseq1hash  10547  fiprsshashgt1  10563  fimaxq  10573  fnfz0hash  10575  ffzo0hash  10577  zfz1isolemiso  10582  zfz1iso  10584  seq3coll  10585  shftfvalg  10590  ovshftex  10591  shftdm  10594  shftfib  10595  shftval  10597  shftval5  10601  shftf  10602  2shfti  10603  seq3shft  10610  crre  10629  rereb  10635  cjreim2  10676  cjap  10678  caucvgrelemrec  10751  caucvgrelemcau  10752  caucvgre  10753  cvg1nlemf  10755  cvg1nlemres  10757  uzin2  10759  rexuz3  10762  recvguniq  10767  sqrt0  10776  resqrexlemdecn  10784  resqrexlemlo  10785  resqrexlemcalc3  10788  resqrexlemnm  10790  resqrexlemcvg  10791  resqrexlemoverl  10793  resqrexlemglsq  10794  resqrexlemga  10795  resqrex  10798  sqrtgt0  10806  absrpclap  10833  absext  10835  absmul  10841  leabs  10846  nn0abscl  10857  ltabs  10859  abslt  10860  absle  10861  abssubap0  10862  abstri  10876  cau3lem  10886  caubnd2  10889  maxabsle  10976  maxabslemlub  10979  maxabslemval  10980  maxcl  10982  maxleastb  10986  maxltsup  10990  rexanre  10992  rexico  10993  zmaxcl  10996  2zsupmax  10997  fimaxre2  10998  minmax  11001  min2inf  11004  minabs  11007  minclpr  11008  mul0inf  11012  xrmaxiflemcl  11014  xrmaxifle  11015  xrmaxiflemab  11016  xrmaxiflemlub  11017  xrmaxiflemcom  11018  xrmaxiflemval  11019  xrltmaxsup  11026  xrmaxltsup  11027  xrmaxaddlem  11029  xrmaxadd  11030  xrnegiso  11031  xrminmax  11034  xrbdtri  11045  clim  11050  climi2  11057  climconst2  11060  climuni  11062  climmpt  11069  climshftlemg  11071  climres  11072  climcn1  11077  subcn2  11080  cn1lem  11083  climadd  11095  climmul  11096  climsub  11097  climle  11103  climsqz  11104  climsqz2  11105  clim2ser  11106  clim2ser2  11107  iserex  11108  isermulc2  11109  iserle  11111  iserge0  11112  climub  11113  climrecvg1n  11117  climcvg1nlem  11118  serf0  11121  sumeq2  11128  sumfct  11143  sumrbdclem  11146  fsum3cvg  11147  sumrbdc  11148  summodclem2a  11150  summodclem2  11151  summodc  11152  zsumdc  11153  isum  11154  fsum3  11156  sum0  11157  isumz  11158  fsumf1o  11159  isumss  11160  fisumss  11161  isumss2  11162  fsum3cvg2  11163  fsum3cvg3  11165  fsum3ser  11166  fsumcl2lem  11167  fsumcllem  11168  fsumadd  11175  fsumsplit  11176  sumsnf  11178  isumclim3  11192  isummulc2  11195  isumadd  11200  fsum2dlemstep  11203  fsum2d  11204  fisumcom2  11207  fsum0diaglem  11209  fsumrev  11212  fsumshft  11213  fisumrev2  11215  fsummulc2  11217  fsumconst  11223  modfsummod  11227  fsum00  11231  fsumabs  11234  telfsumo  11235  fsumparts  11239  fsumrelem  11240  iserabs  11244  cvgcmpub  11245  fsumiun  11246  binom1dif  11256  bcxmas  11258  isumshft  11259  isumlessdc  11265  divcnv  11266  trireciplem  11269  trirecip  11270  expcnvap0  11271  expcnvre  11272  expcnv  11273  explecnv  11274  geolim  11280  geolim2  11281  geo2sum  11283  geo2lim  11285  geoisum  11286  geoisumr  11287  geoisum1  11288  geoisum1c  11289  cvgratnnlemnexp  11293  cvgratnnlemseq  11295  cvgratz  11301  mertenslem2  11305  mertensabs  11306  clim2prod  11308  clim2divap  11309  prodfdivap  11316  prodeq2  11326  prodrbdclem  11340  fproddccvg  11341  prodrbdclem2  11342  prodmodclem3  11344  prodmodclem2a  11345  prodmodc  11347  eftvalcn  11363  ef0lem  11366  efcvgfsum  11373  ege2le3  11377  efcj  11379  efaddlem  11380  efadd  11381  eftlcvg  11393  eftlub  11396  efler  11405  eflegeo  11408  tanvalap  11415  tanclap  11416  tanval2ap  11420  tanval3ap  11421  tannegap  11435  sinadd  11443  cosadd  11444  eirrap  11484  dvdsval2  11496  dvdsdc  11501  moddvds  11502  zdvdsdc  11514  dvdscmul  11520  dvdsmulc  11521  dvdscmulr  11522  dvdsmulcr  11523  modmulconst  11525  dvdsadd  11536  dvdsadd2b  11540  dvdslelemd  11541  dvdsle  11542  dvdsabseq  11545  dvdseq  11546  divconjdvds  11547  dvds1  11551  fzo0dvdseq  11555  dvdsmod  11560  oddm1even  11572  mod2eq1n2dvds  11576  evennn02n  11579  evennn2n  11580  divalglemnn  11615  divalglemnqt  11617  divalglemeunn  11618  divalglemex  11619  divalglemeuneg  11620  divalg  11621  divalgmod  11624  modremain  11626  infssuzex  11642  gcdsupex  11646  gcdsupcl  11647  gcdval  11648  dvdslegcd  11653  gcdnncl  11656  gcdneg  11670  gcdaddm  11672  gcd1  11675  bezoutlemnewy  11684  bezoutlemmain  11686  bezoutlemex  11689  bezoutlemzz  11690  bezoutlemaz  11691  bezoutlembz  11692  bezoutlembi  11693  bezoutlemle  11696  bezoutlemsup  11697  gcdass  11703  gcdzeq  11710  dvdsmulgcd  11713  bezoutr1  11721  algrp1  11727  algcvga  11732  eucalgval2  11734  eucalgf  11736  eucalglt  11738  lcmval  11744  lcmledvds  11751  lcmneg  11755  lcmgcd  11759  lcmid  11761  coprmgcdb  11769  ncoprmgcdne1b  11770  mulgcddvds  11775  rpmulgcd2  11776  qredeq  11777  divgcdcoprm0  11782  divgcdcoprmex  11783  cncongr1  11784  cncongr2  11785  isprm2lem  11797  prmind2  11801  sqnprm  11816  isprm6  11825  prmdvdsexp  11826  prmfac1  11830  rpexp  11831  rpexp1i  11832  sqrt2irr  11840  pw2dvdslemn  11843  pw2dvdseulemle  11845  oddpwdclemxy  11847  oddpwdclemdc  11851  oddpwdc  11852  znege1  11856  sqrt2irraplemnn  11857  sqrt2irrap  11858  divnumden  11874  qden1elz  11883  phibndlem  11892  dfphi2  11896  phiprmpw  11898  crth  11900  phimullem  11901  oddennn  11905  evenennn  11906  ennnfonelemk  11913  ennnfonelemg  11916  ennnfonelemss  11923  ennnfoneleminc  11924  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ennnfonelemex  11927  ennnfonelemhom  11928  ennnfonelemrnh  11929  ennnfonelemfun  11930  ennnfonelemf1  11931  ennnfonelemrn  11932  ennnfonelemdm  11933  ennnfonelemnn0  11935  exmidunben  11939  ctinfomlemom  11940  ctinfom  11941  ctinf  11943  ctiunctlemudc  11950  ctiunctlemf  11951  ctiunct  11953  unct  11954  isstruct2im  11969  isstruct2r  11970  setsvalg  11989  setsslid  12009  ressid2  12018  ressval2  12019  2strbasg  12060  2stropg  12061  2strop1g  12064  restval  12126  restid2  12129  eltg3i  12225  bastg  12230  topbas  12236  tgtop  12237  tgidm  12243  tgss2  12248  bastop2  12253  epttop  12259  iuncld  12284  clsss2  12298  isopn3i  12304  neiint  12314  neii2  12318  neissex  12334  restbasg  12337  tgrest  12338  resttopon  12340  ssrest  12351  restopn2  12352  lmfval  12361  cnpval  12367  lmcvg  12386  iscnp4  12387  cncnpi  12397  cnconst2  12402  cnrest  12404  cnrest2  12405  cnrest2r  12406  cnptopresti  12407  cnptoprest  12408  cnptoprest2  12409  lmss  12415  lmtopcnp  12419  txcnp  12440  upxp  12441  uptx  12443  txcn  12444  txlm  12448  cnmpt11  12452  cnmpt1t  12454  hmeores  12484  txswaphmeo  12490  psmetres2  12502  ismet2  12523  xmettri2  12530  xmetres2  12548  metres2  12550  blfvalps  12554  bldisj  12570  xblss2ps  12573  xblss2  12574  xblm  12586  blssps  12596  blss  12597  metss2lem  12666  metss2  12667  bdxmet  12670  bdbl  12672  metrest  12675  xmetxpbl  12677  xmettxlem  12678  xmettx  12679  metcnp3  12680  metcnp2  12682  metcnpi  12684  metcnpi2  12685  txmetcnp  12687  qtopbas  12691  tgioo  12715  addcncntoplem  12720  fsumcncntop  12725  rescncf  12737  cncfco  12747  cncfcncntop  12749  cncfmptid  12752  addccncf  12755  cdivcncfap  12756  negcncf  12757  mulcncflem  12759  mulcncf  12760  dedekindeulemuub  12764  dedekindeulemloc  12766  dedekindeulemlu  12768  dedekindeulemeu  12769  dedekindeu  12770  suplociccreex  12771  suplociccex  12772  dedekindicclemuub  12773  dedekindicclemloc  12775  dedekindicclemlu  12777  dedekindicclemeu  12778  dedekindicclemicc  12779  ivthinclemlopn  12783  ivthinclemlr  12784  ivthinclemuopn  12785  ivthinclemur  12786  ivthinclemloc  12788  ivthinc  12790  limccl  12797  ellimc3apf  12798  limcdifap  12800  limcmpted  12801  limcimolemlt  12802  limcimo  12803  cnplimcim  12805  cnplimclemle  12806  cnplimclemr  12807  cnlimcim  12809  limccnpcntop  12813  limccoap  12816  reldvg  12817  dvfvalap  12819  dvfgg  12826  dvidlemap  12829  dvcnp2cntop  12832  dvcjbr  12841  dvcj  12842  dvfre  12843  dvexp  12844  dvrecap  12846  dveflem  12855  dvef  12856  sin0pilem1  12862  sin0pilem2  12863  pilem3  12864  ptolemy  12905  coseq0q4123  12915  coseq0negpitopi  12917  cos02pilt1  12932  bj-nnan  12948  bj-indind  13130  bj-omtrans  13154  pwtrufal  13192  pwle2  13193  pwf1oexmid  13194  subctctexmid  13196  nnsf  13199  peano4nninf  13200  nninfalllemn  13202  nninfalllem1  13203  nninfall  13204  nninfself  13209  nninfsellemeq  13210  nninfsellemqall  13211  nninfsellemeqinf  13212  nninfsel  13213  nninfomnilem  13214  nninffeq  13216  sbthom  13221  qdencn  13222  refeq  13223  isomninnlem  13225  trilpolemclim  13229  trilpolemcl  13230  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234  trilpolemres  13235  taupi  13239