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  342  simpl2im  384  sylancom  417  adantll  468  adantrl  470  adantlll  472  adantlrl  474  adantrll  476  adantrrl  478  simpllr  524  simplrr  526  simprlr  528  simprrr  530  anabs7  564  jcab  593  pm4.38  595  pm5.21  685  ioran  742  pm3.14  743  ordi  806  pm4.39  812  pm5.16  814  pm5.54dc  904  intnan  915  intnand  917  dcan  919  bimsc1  948  niabn  952  simp1r  1007  simp2r  1009  simp3r  1011  3anandirs  1327  bilukdc  1375  19.26  1458  exsimpr  1598  19.40  1611  cbvexh  1729  sbequilem  1811  spsbe  1815  cbvexdh  1899  euan  2056  moan  2069  datisi  2110  fresison  2118  rexex  2482  r19.26  2561  r19.29an  2577  r19.40  2588  cbvraldva2  2664  cbvrexdva2  2665  gencbvex  2735  rspct  2786  rspcimdv  2794  rspcimedv  2795  rr19.28v  2828  elrab3t  2843  reu6  2877  rmob  3005  csbiebt  3044  rabssab  3189  ssddif  3315  difin  3318  difrab  3355  dcun  3478  eqifdc  3511  ifmdc  3514  preqsn  3710  opprc2  3736  dfnfc2  3762  intmin4  3807  sndisj  3933  undifexmid  4125  exmid01  4129  pwntru  4130  exmidn0m  4132  exmidsssn  4133  exmidsssnc  4134  exmidundif  4137  exmidundifim  4138  exss  4157  euotd  4184  frirrg  4280  suctr  4351  abnexg  4375  ordtri2or2exmid  4494  wetriext  4499  reg3exmidlemwe  4501  tfisi  4509  peano2  4517  omsinds  4543  nnpredcl  4544  relop  4697  releldm  4782  relelrn  4783  resiexg  4872  trin2  4938  xpmlem  4967  unielrel  5074  relcoi2  5077  iota2df  5120  iota2  5122  funopab4  5168  fun11uni  5201  imadiflem  5210  imain  5213  fneq12  5224  f1ssr  5343  fvelrnb  5477  ssimaex  5490  fvmpt2d  5515  fvmptdf  5516  dffo3  5575  ffvresb  5591  fmptco  5594  funfvima3  5659  f1imass  5683  fliftf  5708  fliftval  5709  riota2df  5758  riota5f  5762  acexmidlemcase  5777  ovprc2  5816  eloprabga  5866  eqfnov2  5886  ovmpodxf  5904  ofvalg  5999  offval2  6005  ofrfval2  6006  caofinvl  6012  2ndrn  6089  1st2ndbr  6090  cnvf1o  6130  f1o2ndf1  6133  mpoxopoveq  6145  dftpos4  6168  tpostpos  6169  tposf12  6174  dfsmo2  6192  smores  6197  tfrlem1  6213  tfrlem3ag  6214  tfrlem3a  6215  tfrlemisucaccv  6230  tfrlemi1  6237  tfrexlem  6239  tfr1onlem3ag  6242  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfr1onlemaccex  6253  tfr1onlemres  6254  tfri1dALT  6256  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcllemaccex  6266  tfrcllemres  6267  tfrcl  6269  rdgivallem  6286  rdgon  6291  frecabex  6303  frecabcl  6304  frectfr  6305  frecrdg  6313  oawordi  6373  nntri3  6401  nntr2  6407  dcdifsnid  6408  nnaordi  6412  nnaordex  6431  nnawordex  6432  nnm00  6433  ersymb  6451  ertr  6452  erref  6457  iserd  6463  swoer  6465  erth  6481  iinerm  6509  erinxp  6511  ecinxp  6512  qsel  6514  qliftel  6517  qliftfun  6519  fvdiagfn  6595  ixpssmapg  6630  resixp  6635  mptelixpg  6636  dom3  6678  ssdomg  6680  cnven  6710  xpen  6747  xpmapenlem  6751  ssenen  6753  phplem4dom  6764  phpm  6767  phpelm  6768  fidifsnen  6772  fin0  6787  fin0or  6788  isinfinf  6799  tridc  6801  fimax2gtrilemstep  6802  fimax2gtri  6803  finexdc  6804  en2eqpr  6809  fientri3  6811  unsnfidcex  6816  unsnfidcel  6817  unfidisj  6818  undifdcss  6819  undifdc  6820  unfiin  6822  fiintim  6825  fnfi  6833  relcnvfi  6837  f1dmvrnfibi  6840  iunfidisj  6842  f1finf1o  6843  fidcenumlemrks  6849  fidcenumlemr  6851  fidcenum  6852  fival  6866  elfi2  6868  ssfii  6870  fiss  6873  suplubti  6895  suplub2ti  6896  supelti  6897  supisolem  6903  supisoex  6904  infglbti  6920  ordiso2  6928  djuss  6963  updjudhcoinlf  6973  updjudhcoinrg  6974  updjud  6975  djudom  6986  omp1eomlem  6987  difinfsnlem  6992  difinfsn  6993  difinfinf  6994  ctm  7002  ctssdclemn0  7003  ctssdccl  7004  ctssdc  7006  enumctlemm  7007  enumct  7008  enomnilem  7018  finomni  7020  exmidomni  7022  fodjuomnilemdc  7024  fodjuomnilemres  7028  nnnninf  7031  ctssexmid  7032  ismkvnex  7037  mkvprop  7040  fodjumkvlemres  7041  enmkvlem  7043  omniwomnimkv  7049  enwomnilem  7050  en2eleq  7068  en2other2  7069  exmidfodomrlemeldju  7072  exmidfodomrlemreseldju  7073  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  exmidaclem  7081  dju1en  7086  djudomr  7093  cc2lem  7098  cc3  7100  dmaddpqlem  7209  nqpi  7210  mulcanenq  7217  ltaddnq  7239  ltexnqq  7240  prarloclemarch2  7251  ltrnqg  7252  ltnnnq  7255  enq0sym  7264  nqnq0pi  7270  nq0nn  7274  mulcanenq0ec  7277  addnq0mo  7279  mulnq0mo  7280  addnnnq0  7281  prloc  7323  prarloclemlt  7325  prarloclemlo  7326  ltdfpr  7338  genplt2i  7342  genpml  7349  genpmu  7350  addnqprllem  7359  addnqprulem  7360  addnqprl  7361  addnqpru  7362  nqprloc  7377  appdivnq  7395  appdiv0nq  7396  mulnqprl  7400  mulnqpru  7401  distrlem1prl  7414  distrlem1pru  7415  ltprordil  7421  1idprl  7422  1idpru  7423  ltexprlemrl  7442  ltexprlemru  7444  ltexpri  7445  addcanprleml  7446  addcanprlemu  7447  recexprlem1ssl  7465  recexpr  7470  aptiprlemu  7472  archpr  7475  cauappcvgprlemopl  7478  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemloc  7507  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprlemlim  7513  caucvgprprlemval  7520  caucvgprprlemml  7526  caucvgprprlemopl  7529  caucvgprprlemopu  7531  caucvgprprlemloc  7535  caucvgprprlemexbt  7538  caucvgprprlemexb  7539  caucvgprprlemaddq  7540  caucvgprprlemlim  7543  suplocexprlemru  7551  suplocexprlemloc  7553  suplocexprlemub  7555  suplocexprlemlub  7556  addsrmo  7575  mulsrmo  7576  addsrpr  7577  mulsrpr  7578  0idsr  7599  1idsr  7600  recexsrlem  7606  addgt0sr  7607  srpospr  7615  prsradd  7618  prsrlt  7619  caucvgsrlemfv  7623  caucvgsrlemgt1  7627  caucvgsrlemoffval  7628  caucvgsrlemoffcau  7630  caucvgsrlemoffres  7632  mappsrprg  7636  map2psrprg  7637  suplocsrlemb  7638  suplocsrlem  7640  suplocsr  7641  rereceu  7721  axarch  7723  nntopi  7726  axcaucvglemval  7729  axpre-suploclemres  7733  axpre-suploc  7734  axsuploc  7861  muladd11r  7942  cnegexlem1  7961  cnegex  7964  negeu  7977  pncan  7992  pncan3  7994  npcan  7995  addid0  8159  negf1o  8168  mulneg1  8181  lelttrdi  8212  ltnegcon2  8250  add20  8260  subge0  8261  lesub0  8265  reapval  8362  recexre  8364  apreap  8373  ltmul1a  8377  reapneg  8383  cru  8388  apsym  8392  apcotr  8393  apadd1  8394  apneg  8397  mulext1  8398  apti  8408  gt0ap0  8412  ap0gt0  8426  subap0  8429  lt0ap0  8434  recexap  8438  divmulassap  8479  divmulasscomap  8480  rerecclap  8514  recgt0  8632  prodgt0gt0  8633  lemul1a  8640  lemul12a  8644  lt2msq  8668  ltrec1  8670  recreclt  8682  negiso  8737  sup3exmid  8739  creui  8742  cju  8743  avglt2  8983  un0addcl  9034  nn0ge2m1nn  9061  nn0nndivcl  9063  elnn0z  9091  peano2z  9114  elz2  9146  suprzclex  9173  peano5uzti  9183  zindd  9193  btwnapz  9205  eluzadd  9378  nn0pzuz  9409  supinfneg  9417  infsupneg  9418  eluz2b2  9424  eqreznegel  9433  nn0ge2m1nnALT  9437  divfnzn  9440  qmulz  9442  qapne  9458  qreccl  9461  cnref1o  9469  ge0p1rp  9502  mul2lt0rlt0  9576  mul2lt0rgt0  9577  xrltso  9612  npnflt  9628  nmnfgt  9631  z2ge  9639  xltnegi  9648  xaddval  9658  xaddcom  9674  xnegdi  9681  xaddass  9682  xpncan  9684  xleadd1a  9686  xltadd1  9689  xlt2add  9693  xsubge0  9694  xposdif  9695  xlesubadd  9696  xleaddadd  9700  ixxssixx  9715  lincmb01cmp  9816  iccf1o  9817  zltaddlt1le  9820  fztri3or  9850  fzdcel  9851  fznlem  9852  fzn  9853  uzsubsubfz  9858  fzsplit2  9861  fzopth  9872  fzdifsuc  9892  fzrev2i  9897  elfz1b  9901  fzneuz  9912  fzrevral  9916  ige2m1fz  9921  elfz0ubfz0  9933  elfz0fzfz0  9934  4fvwrd4  9948  2ffzeq  9949  fzospliti  9984  fzosplit  9985  fzo1fzo0n0  9991  fzonmapblen  9995  fzoaddel  10000  fzosubel  10002  fzosubel3  10004  elfzodifsumelfzo  10009  elfzom1elp1fzo  10010  elfzom1p1elfzo  10022  elfzonelfzo  10038  peano2fzor  10040  exfzdc  10048  fvinim0ffz  10049  qtri3or  10051  exbtwnzlemstep  10056  rebtwn2zlemstep  10061  qbtwnxr  10066  apbtwnz  10078  flqge  10086  flqltnz  10091  flqaddz  10101  btwnzge0  10104  flltdivnn0lt  10108  intfracq  10124  flqdiv  10125  modqid0  10154  q0mod  10159  q1mod  10160  modqmuladdim  10171  modqmuladdnn0  10172  q2txmodxeq0  10188  q2submod  10189  modifeq2int  10190  modqsubdir  10197  modsumfzodifsn  10200  addmodlteq  10202  frec2uzzd  10204  frec2uzuzd  10206  frec2uzrand  10209  frec2uzf1od  10210  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdgtcl  10216  frecuzrdgsuc  10218  frecuzrdgg  10220  frecuzrdgdomlem  10221  frecuzrdgfunlem  10223  frecuzrdgsuctlem  10227  frecfzennn  10230  uzsinds  10246  seq3val  10262  seqvalcd  10263  seq3clss  10271  seq3feq2  10274  seq3feq  10276  ser3mono  10282  seq3split  10283  iseqf1olemkle  10288  iseqf1olemklt  10289  iseqf1olemqcl  10290  iseqf1olemnab  10292  iseqf1olemab  10293  iseqf1olemqf  10295  iseqf1olemmo  10296  iseqf1olemqf1o  10297  iseqf1olemqk  10298  iseqf1olemjpcl  10299  iseqf1olemqpcl  10300  iseqf1olemfvp  10301  seq3f1olemqsumkj  10302  seq3f1olemqsumk  10303  seq3f1olemqsum  10304  seq3f1oleml  10307  seq3f1o  10308  seq3id3  10311  seq3id  10312  seq3homo  10314  seq3z  10315  seqfeq3  10316  fser0const  10320  ser3ge0  10321  exp3vallem  10325  exp3val  10326  expnnval  10327  expp1  10331  rpexpcl  10343  expaddzaplem  10367  leexp1a  10379  exple1  10380  subsq  10430  binom2  10434  binom3  10440  bernneq3  10445  expnbnd  10446  expcan  10494  apexp1  10496  nn0opthd  10500  faclbnd  10519  faclbnd6  10522  facubnd  10523  facavg  10524  bcval  10527  bccmpl  10532  bcval5  10541  bcpasc  10544  hashennnuni  10557  hashennn  10558  hashfiv01gt1  10560  fihasheqf1oi  10566  hashnncl  10574  fseq1hash  10579  fiprsshashgt1  10595  fimaxq  10605  fnfz0hash  10607  ffzo0hash  10609  zfz1isolemiso  10614  zfz1iso  10616  seq3coll  10617  shftfvalg  10622  ovshftex  10623  shftdm  10626  shftfib  10627  shftval  10629  shftval5  10633  shftf  10634  2shfti  10635  seq3shft  10642  crre  10661  rereb  10667  cjreim2  10708  cjap  10710  caucvgrelemrec  10783  caucvgrelemcau  10784  caucvgre  10785  cvg1nlemf  10787  cvg1nlemres  10789  uzin2  10791  rexuz3  10794  recvguniq  10799  sqrt0  10808  resqrexlemdecn  10816  resqrexlemlo  10817  resqrexlemcalc3  10820  resqrexlemnm  10822  resqrexlemcvg  10823  resqrexlemoverl  10825  resqrexlemglsq  10826  resqrexlemga  10827  resqrex  10830  sqrtgt0  10838  absrpclap  10865  absext  10867  absmul  10873  leabs  10878  nn0abscl  10889  ltabs  10891  abslt  10892  absle  10893  abssubap0  10894  abstri  10908  cau3lem  10918  caubnd2  10921  maxabsle  11008  maxabslemlub  11011  maxabslemval  11012  maxcl  11014  maxleastb  11018  maxltsup  11022  rexanre  11024  rexico  11025  zmaxcl  11028  2zsupmax  11029  fimaxre2  11030  minmax  11033  min2inf  11036  minabs  11039  minclpr  11040  mul0inf  11044  xrmaxiflemcl  11046  xrmaxifle  11047  xrmaxiflemab  11048  xrmaxiflemlub  11049  xrmaxiflemcom  11050  xrmaxiflemval  11051  xrltmaxsup  11058  xrmaxltsup  11059  xrmaxaddlem  11061  xrmaxadd  11062  xrnegiso  11063  xrminmax  11066  xrbdtri  11077  clim  11082  climi2  11089  climconst2  11092  climuni  11094  climmpt  11101  climshftlemg  11103  climres  11104  climcn1  11109  subcn2  11112  cn1lem  11115  climadd  11127  climmul  11128  climsub  11129  climle  11135  climsqz  11136  climsqz2  11137  clim2ser  11138  clim2ser2  11139  iserex  11140  isermulc2  11141  iserle  11143  iserge0  11144  climub  11145  climrecvg1n  11149  climcvg1nlem  11150  serf0  11153  sumeq2  11160  sumfct  11175  sumrbdclem  11178  fsum3cvg  11179  sumrbdc  11180  summodclem2a  11182  summodclem2  11183  summodc  11184  zsumdc  11185  isum  11186  fsum3  11188  sum0  11189  isumz  11190  fsumf1o  11191  isumss  11192  fisumss  11193  isumss2  11194  fsum3cvg2  11195  fsum3cvg3  11197  fsum3ser  11198  fsumcl2lem  11199  fsumcllem  11200  fsumadd  11207  fsumsplit  11208  sumsnf  11210  isumclim3  11224  isummulc2  11227  isumadd  11232  fsum2dlemstep  11235  fsum2d  11236  fisumcom2  11239  fsum0diaglem  11241  fsumrev  11244  fsumshft  11245  fisumrev2  11247  fsummulc2  11249  fsumconst  11255  modfsummod  11259  fsum00  11263  fsumabs  11266  telfsumo  11267  fsumparts  11271  fsumrelem  11272  iserabs  11276  cvgcmpub  11277  fsumiun  11278  binom1dif  11288  bcxmas  11290  isumshft  11291  isumlessdc  11297  divcnv  11298  trireciplem  11301  trirecip  11302  expcnvap0  11303  expcnvre  11304  expcnv  11305  explecnv  11306  geolim  11312  geolim2  11313  geo2sum  11315  geo2lim  11317  geoisum  11318  geoisumr  11319  geoisum1  11320  geoisum1c  11321  cvgratnnlemnexp  11325  cvgratnnlemseq  11327  cvgratz  11333  mertenslem2  11337  mertensabs  11338  clim2prod  11340  clim2divap  11341  prodfdivap  11348  prodeq2  11358  prodrbdclem  11372  fproddccvg  11373  prodrbdclem2  11374  prodmodclem3  11376  prodmodclem2a  11377  prodmodc  11379  zproddc  11380  fprodseq  11384  eftvalcn  11400  ef0lem  11403  efcvgfsum  11410  ege2le3  11414  efcj  11416  efaddlem  11417  efadd  11418  eftlcvg  11430  eftlub  11433  eflegeo  11444  tanvalap  11451  tanclap  11452  tanval2ap  11456  tanval3ap  11457  tannegap  11471  sinadd  11479  cosadd  11480  eirrap  11520  dvdsval2  11532  dvdsdc  11537  moddvds  11538  zdvdsdc  11550  dvdscmul  11556  dvdsmulc  11557  dvdscmulr  11558  dvdsmulcr  11559  modmulconst  11561  dvdsadd  11572  dvdsadd2b  11576  dvdslelemd  11577  dvdsle  11578  dvdsabseq  11581  dvdseq  11582  divconjdvds  11583  dvds1  11587  fzo0dvdseq  11591  dvdsmod  11596  oddm1even  11608  mod2eq1n2dvds  11612  evennn02n  11615  evennn2n  11616  divalglemnn  11651  divalglemnqt  11653  divalglemeunn  11654  divalglemex  11655  divalglemeuneg  11656  divalg  11657  divalgmod  11660  modremain  11662  infssuzex  11678  gcdsupex  11682  gcdsupcl  11683  gcdval  11684  dvdslegcd  11689  gcdnncl  11692  gcdneg  11706  gcdaddm  11708  gcd1  11711  bezoutlemnewy  11720  bezoutlemmain  11722  bezoutlemex  11725  bezoutlemzz  11726  bezoutlemaz  11727  bezoutlembz  11728  bezoutlembi  11729  bezoutlemle  11732  bezoutlemsup  11733  gcdass  11739  gcdzeq  11746  dvdsmulgcd  11749  bezoutr1  11757  algrp1  11763  algcvga  11768  eucalgval2  11770  eucalgf  11772  eucalglt  11774  lcmval  11780  lcmledvds  11787  lcmneg  11791  lcmgcd  11795  lcmid  11797  coprmgcdb  11805  ncoprmgcdne1b  11806  mulgcddvds  11811  rpmulgcd2  11812  qredeq  11813  divgcdcoprm0  11818  divgcdcoprmex  11819  cncongr1  11820  cncongr2  11821  isprm2lem  11833  prmind2  11837  sqnprm  11852  isprm6  11861  prmdvdsexp  11862  prmfac1  11866  rpexp  11867  rpexp1i  11868  sqrt2irr  11876  pw2dvdslemn  11879  pw2dvdseulemle  11881  oddpwdclemxy  11883  oddpwdclemdc  11887  oddpwdc  11888  znege1  11892  sqrt2irraplemnn  11893  sqrt2irrap  11894  divnumden  11910  qden1elz  11919  phibndlem  11928  dfphi2  11932  phiprmpw  11934  crth  11936  phimullem  11937  oddennn  11941  evenennn  11942  ennnfonelemk  11949  ennnfonelemg  11952  ennnfonelemss  11959  ennnfoneleminc  11960  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemex  11963  ennnfonelemhom  11964  ennnfonelemrnh  11965  ennnfonelemfun  11966  ennnfonelemf1  11967  ennnfonelemrn  11968  ennnfonelemdm  11969  ennnfonelemnn0  11971  exmidunben  11975  ctinfomlemom  11976  ctinfom  11977  ctinf  11979  ctiunctlemudc  11986  ctiunctlemf  11987  ctiunct  11989  unct  11991  omctfn  11992  omiunct  11993  isstruct2im  12008  isstruct2r  12009  setsvalg  12028  setsslid  12048  ressid2  12057  ressval2  12058  2strbasg  12099  2stropg  12100  2strop1g  12103  restval  12165  restid2  12168  eltg3i  12264  bastg  12269  topbas  12275  tgtop  12276  tgidm  12282  tgss2  12287  bastop2  12292  epttop  12298  iuncld  12323  clsss2  12337  isopn3i  12343  neiint  12353  neii2  12357  neissex  12373  restbasg  12376  tgrest  12377  resttopon  12379  ssrest  12390  restopn2  12391  lmfval  12400  cnpval  12406  lmcvg  12425  iscnp4  12426  cncnpi  12436  cnconst2  12441  cnrest  12443  cnrest2  12444  cnrest2r  12445  cnptopresti  12446  cnptoprest  12447  cnptoprest2  12448  lmss  12454  lmtopcnp  12458  txcnp  12479  upxp  12480  uptx  12482  txcn  12483  txlm  12487  cnmpt11  12491  cnmpt1t  12493  hmeores  12523  txswaphmeo  12529  psmetres2  12541  ismet2  12562  xmettri2  12569  xmetres2  12587  metres2  12589  blfvalps  12593  bldisj  12609  xblss2ps  12612  xblss2  12613  xblm  12625  blssps  12635  blss  12636  metss2lem  12705  metss2  12706  bdxmet  12709  bdbl  12711  metrest  12714  xmetxpbl  12716  xmettxlem  12717  xmettx  12718  metcnp3  12719  metcnp2  12721  metcnpi  12723  metcnpi2  12724  txmetcnp  12726  qtopbas  12730  tgioo  12754  addcncntoplem  12759  fsumcncntop  12764  rescncf  12776  cncfco  12786  cncfcncntop  12788  cncfmptid  12791  addccncf  12794  cdivcncfap  12795  negcncf  12796  mulcncflem  12798  mulcncf  12799  dedekindeulemuub  12803  dedekindeulemloc  12805  dedekindeulemlu  12807  dedekindeulemeu  12808  dedekindeu  12809  suplociccreex  12810  suplociccex  12811  dedekindicclemuub  12812  dedekindicclemloc  12814  dedekindicclemlu  12816  dedekindicclemeu  12817  dedekindicclemicc  12818  ivthinclemlopn  12822  ivthinclemlr  12823  ivthinclemuopn  12824  ivthinclemur  12825  ivthinclemloc  12827  ivthinc  12829  limccl  12836  ellimc3apf  12837  limcdifap  12839  limcmpted  12840  limcimolemlt  12841  limcimo  12842  cnplimcim  12844  cnplimclemle  12845  cnplimclemr  12846  cnlimcim  12848  limccnpcntop  12852  limccoap  12855  reldvg  12856  dvfvalap  12858  dvfgg  12865  dvidlemap  12868  dvcnp2cntop  12871  dvcjbr  12880  dvcj  12881  dvfre  12882  dvexp  12883  dvrecap  12885  dveflem  12895  dvef  12896  reeff1olem  12900  reeff1o  12902  efltlemlt  12903  eflt  12904  sin0pilem1  12910  sin0pilem2  12911  pilem3  12912  ptolemy  12953  coseq0q4123  12963  coseq0negpitopi  12965  cos02pilt1  12980  cos11  12982  relogeftb  12994  rplogcl  13008  logge0  13009  logdivlti  13010  rpcxpef  13023  rpcncxpcl  13031  rpcxpcl  13032  cxpap0  13033  rpcxpneg  13036  cxprec  13039  abscxp  13043  relogbval  13076  relogbzcl  13077  nnlogbexp  13084  logbrec  13085  logbgcd1irr  13092  logbgcd1irraplemexp  13093  logbgcd1irrap  13095  bj-nnan  13119  bj-indind  13301  bj-omtrans  13325  pwtrufal  13365  pwle2  13366  pwf1oexmid  13367  subctctexmid  13369  pw1nct  13371  nnsf  13374  peano4nninf  13375  nninfalllemn  13377  nninfalllem1  13378  nninfall  13379  nninfself  13384  nninfsellemeq  13385  nninfsellemqall  13386  nninfsellemeqinf  13387  nninfsel  13388  nninfomnilem  13389  nninffeq  13391  sbthom  13396  qdencn  13397  refeq  13398  isomninnlem  13400  trilpolemclim  13404  trilpolemcl  13405  trilpolemisumle  13406  trilpolemeq1  13408  trilpolemlt1  13409  trilpolemres  13410  trirec0  13412  trirec0xor  13413  apdifflemf  13414  apdifflemr  13415  apdiff  13416  iswomninnlem  13417  ismkvnnlem  13419  redcwlpolemeq1  13421  neapmkvlem  13424  taupi  13430