ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simpr Unicode version

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
StepHypRef Expression
1 ax-ia2 106 1  |-  ( (
ph  /\  ps )  ->  ps )
Colors of variables: wff set class
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  508  simplrr  510  simprlr  512  simprrr  514  anabs7  548  jcab  577  pm4.38  579  pm5.21  669  ioran  726  pm3.14  727  ordi  790  pm4.39  796  pm5.16  798  pm5.54dc  888  intnan  899  intnand  901  dcan  903  bimsc1  932  niabn  936  simp1r  991  simp2r  993  simp3r  995  3anandirs  1311  bilukdc  1359  19.26  1442  exsimpr  1582  19.40  1595  cbvexh  1713  sbequilem  1794  spsbe  1798  cbvexdh  1878  euan  2033  moan  2046  datisi  2087  fresison  2095  rexex  2456  r19.26  2535  r19.29an  2551  r19.40  2562  cbvraldva2  2635  cbvrexdva2  2636  gencbvex  2706  rspct  2756  rspcimdv  2764  rspcimedv  2765  rr19.28v  2798  elrab3t  2812  reu6  2846  rmob  2973  csbiebt  3009  rabssab  3154  ssddif  3280  difin  3283  difrab  3320  dcun  3443  eqifdc  3476  ifmdc  3479  preqsn  3672  opprc2  3698  dfnfc2  3724  intmin4  3769  sndisj  3895  undifexmid  4087  exmid01  4091  pwntru  4092  exmidn0m  4094  exmidsssn  4095  exmidsssnc  4096  exmidundif  4099  exmidundifim  4100  exss  4119  euotd  4146  frirrg  4242  suctr  4313  abnexg  4337  ordtri2or2exmid  4456  wetriext  4461  reg3exmidlemwe  4463  tfisi  4471  peano2  4479  omsinds  4505  nnpredcl  4506  relop  4659  releldm  4744  relelrn  4745  resiexg  4834  trin2  4900  xpmlem  4929  unielrel  5036  relcoi2  5039  iota2df  5082  iota2  5084  funopab4  5130  fun11uni  5163  imadiflem  5172  imain  5175  fneq12  5186  f1ssr  5305  fvelrnb  5437  ssimaex  5450  fvmpt2d  5475  fvmptdf  5476  dffo3  5535  ffvresb  5551  fmptco  5554  funfvima3  5619  f1imass  5643  fliftf  5668  fliftval  5669  riota2df  5718  riota5f  5722  acexmidlemcase  5737  ovprc2  5776  eloprabga  5826  eqfnov2  5846  ovmpodxf  5864  ofvalg  5959  offval2  5965  ofrfval2  5966  caofinvl  5972  2ndrn  6049  1st2ndbr  6050  cnvf1o  6090  f1o2ndf1  6093  mpoxopoveq  6105  dftpos4  6128  tpostpos  6129  tposf12  6134  dfsmo2  6152  smores  6157  tfrlem1  6173  tfrlem3ag  6174  tfrlem3a  6175  tfrlemisucaccv  6190  tfrlemi1  6197  tfrexlem  6199  tfr1onlem3ag  6202  tfr1onlemsucaccv  6206  tfr1onlembxssdm  6208  tfr1onlembfn  6209  tfr1onlemaccex  6213  tfr1onlemres  6214  tfri1dALT  6216  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllembfn  6222  tfrcllemaccex  6226  tfrcllemres  6227  tfrcl  6229  rdgivallem  6246  rdgon  6251  frecabex  6263  frecabcl  6264  frectfr  6265  frecrdg  6273  oawordi  6333  nntri3  6361  nntr2  6367  dcdifsnid  6368  nnaordi  6372  nnaordex  6391  nnawordex  6392  nnm00  6393  ersymb  6411  ertr  6412  erref  6417  iserd  6423  swoer  6425  erth  6441  iinerm  6469  erinxp  6471  ecinxp  6472  qsel  6474  qliftel  6477  qliftfun  6479  fvdiagfn  6555  ixpssmapg  6590  resixp  6595  mptelixpg  6596  dom3  6638  ssdomg  6640  cnven  6670  xpen  6707  xpmapenlem  6711  ssenen  6713  phplem4dom  6724  phpm  6727  phpelm  6728  fidifsnen  6732  fin0  6747  fin0or  6748  isinfinf  6759  tridc  6761  fimax2gtrilemstep  6762  fimax2gtri  6763  finexdc  6764  en2eqpr  6769  fientri3  6771  unsnfidcex  6776  unsnfidcel  6777  unfidisj  6778  undifdcss  6779  undifdc  6780  unfiin  6782  fiintim  6785  fnfi  6793  relcnvfi  6797  f1dmvrnfibi  6800  iunfidisj  6802  f1finf1o  6803  fidcenumlemrks  6809  fidcenumlemr  6811  fidcenum  6812  fival  6826  elfi2  6828  ssfii  6830  fiss  6833  suplubti  6855  suplub2ti  6856  supelti  6857  supisolem  6863  supisoex  6864  infglbti  6880  ordiso2  6888  djuss  6923  updjudhcoinlf  6933  updjudhcoinrg  6934  updjud  6935  djudom  6946  omp1eomlem  6947  difinfsnlem  6952  difinfsn  6953  difinfinf  6954  ctm  6962  ctssdclemn0  6963  ctssdccl  6964  ctssdc  6966  enumctlemm  6967  enumct  6968  enomnilem  6978  finomni  6980  exmidomni  6982  fodjuomnilemdc  6984  fodjuomnilemres  6988  nnnninf  6991  ctssexmid  6992  ismkvnex  6997  mkvprop  7000  fodjumkvlemres  7001  en2eleq  7019  en2other2  7020  exmidfodomrlemeldju  7023  exmidfodomrlemreseldju  7024  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  exmidaclem  7032  dju1en  7037  djudomr  7044  dmaddpqlem  7153  nqpi  7154  mulcanenq  7161  ltaddnq  7183  ltexnqq  7184  prarloclemarch2  7195  ltrnqg  7196  ltnnnq  7199  enq0sym  7208  nqnq0pi  7214  nq0nn  7218  mulcanenq0ec  7221  addnq0mo  7223  mulnq0mo  7224  addnnnq0  7225  prloc  7267  prarloclemlt  7269  prarloclemlo  7270  ltdfpr  7282  genplt2i  7286  genpml  7293  genpmu  7294  addnqprllem  7303  addnqprulem  7304  addnqprl  7305  addnqpru  7306  nqprloc  7321  appdivnq  7339  appdiv0nq  7340  mulnqprl  7344  mulnqpru  7345  distrlem1prl  7358  distrlem1pru  7359  ltprordil  7365  1idprl  7366  1idpru  7367  ltexprlemrl  7386  ltexprlemru  7388  ltexpri  7389  addcanprleml  7390  addcanprlemu  7391  recexprlem1ssl  7409  recexpr  7414  aptiprlemu  7416  archpr  7419  cauappcvgprlemopl  7422  cauappcvgprlemdisj  7427  cauappcvgprlemloc  7428  cauappcvgprlemladdfu  7430  cauappcvgprlemladdfl  7431  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemloc  7451  caucvgprlemladdfu  7453  caucvgprlemladdrl  7454  caucvgprlemlim  7457  caucvgprprlemval  7464  caucvgprprlemml  7470  caucvgprprlemopl  7473  caucvgprprlemopu  7475  caucvgprprlemloc  7479  caucvgprprlemexbt  7482  caucvgprprlemexb  7483  caucvgprprlemaddq  7484  caucvgprprlemlim  7487  suplocexprlemru  7495  suplocexprlemloc  7497  suplocexprlemub  7499  suplocexprlemlub  7500  addsrmo  7519  mulsrmo  7520  addsrpr  7521  mulsrpr  7522  0idsr  7543  1idsr  7544  recexsrlem  7550  addgt0sr  7551  srpospr  7559  prsradd  7562  prsrlt  7563  caucvgsrlemfv  7567  caucvgsrlemgt1  7571  caucvgsrlemoffval  7572  caucvgsrlemoffcau  7574  caucvgsrlemoffres  7576  mappsrprg  7580  map2psrprg  7581  suplocsrlemb  7582  suplocsrlem  7584  suplocsr  7585  rereceu  7665  axarch  7667  nntopi  7670  axcaucvglemval  7673  axpre-suploclemres  7677  axpre-suploc  7678  axsuploc  7805  muladd11r  7886  cnegexlem1  7905  cnegex  7908  negeu  7921  pncan  7936  pncan3  7938  npcan  7939  addid0  8103  negf1o  8112  mulneg1  8125  lelttrdi  8156  ltnegcon2  8194  add20  8204  subge0  8205  lesub0  8209  reapval  8305  recexre  8307  apreap  8316  ltmul1a  8320  reapneg  8326  cru  8331  apsym  8335  apcotr  8336  apadd1  8337  apneg  8340  mulext1  8341  apti  8351  gt0ap0  8355  ap0gt0  8369  subap0  8372  lt0ap0  8377  recexap  8381  divmulassap  8422  divmulasscomap  8423  rerecclap  8457  recgt0  8572  prodgt0gt0  8573  lemul1a  8580  lemul12a  8584  lt2msq  8608  ltrec1  8610  recreclt  8622  negiso  8677  sup3exmid  8679  creui  8682  cju  8683  avglt2  8917  un0addcl  8968  nn0ge2m1nn  8995  nn0nndivcl  8997  elnn0z  9025  peano2z  9048  elz2  9080  suprzclex  9107  peano5uzti  9117  zindd  9127  btwnapz  9139  eluzadd  9310  nn0pzuz  9338  supinfneg  9346  infsupneg  9347  eluz2b2  9353  eqreznegel  9362  nn0ge2m1nnALT  9366  divfnzn  9369  qmulz  9371  qapne  9387  qreccl  9390  cnref1o  9396  ge0p1rp  9428  mul2lt0rlt0  9501  mul2lt0rgt0  9502  xrltso  9537  npnflt  9553  nmnfgt  9556  z2ge  9564  xltnegi  9573  xaddval  9583  xaddcom  9599  xnegdi  9606  xaddass  9607  xpncan  9609  xleadd1a  9611  xltadd1  9614  xlt2add  9618  xsubge0  9619  xposdif  9620  xlesubadd  9621  xleaddadd  9625  ixxssixx  9640  lincmb01cmp  9741  iccf1o  9742  zltaddlt1le  9744  fztri3or  9774  fzdcel  9775  fznlem  9776  fzn  9777  uzsubsubfz  9782  fzsplit2  9785  fzopth  9796  fzdifsuc  9816  fzrev2i  9821  elfz1b  9825  fzneuz  9836  fzrevral  9840  ige2m1fz  9845  elfz0ubfz0  9857  elfz0fzfz0  9858  4fvwrd4  9872  2ffzeq  9873  fzospliti  9908  fzosplit  9909  fzo1fzo0n0  9915  fzonmapblen  9919  fzoaddel  9924  fzosubel  9926  fzosubel3  9928  elfzodifsumelfzo  9933  elfzom1elp1fzo  9934  elfzom1p1elfzo  9946  elfzonelfzo  9962  peano2fzor  9964  exfzdc  9972  fvinim0ffz  9973  qtri3or  9975  exbtwnzlemstep  9980  rebtwn2zlemstep  9985  qbtwnxr  9990  apbtwnz  10002  flqge  10010  flqltnz  10015  flqaddz  10025  btwnzge0  10028  flltdivnn0lt  10032  intfracq  10048  flqdiv  10049  modqid0  10078  q0mod  10083  q1mod  10084  modqmuladdim  10095  modqmuladdnn0  10096  q2txmodxeq0  10112  q2submod  10113  modifeq2int  10114  modqsubdir  10121  modsumfzodifsn  10124  addmodlteq  10126  frec2uzzd  10128  frec2uzuzd  10130  frec2uzrand  10133  frec2uzf1od  10134  frecuzrdgrrn  10136  frec2uzrdg  10137  frecuzrdgtcl  10140  frecuzrdgsuc  10142  frecuzrdgg  10144  frecuzrdgdomlem  10145  frecuzrdgfunlem  10147  frecuzrdgsuctlem  10151  frecfzennn  10154  uzsinds  10170  seq3val  10186  seqvalcd  10187  seq3clss  10195  seq3feq2  10198  seq3feq  10200  ser3mono  10206  seq3split  10207  iseqf1olemkle  10212  iseqf1olemklt  10213  iseqf1olemqcl  10214  iseqf1olemnab  10216  iseqf1olemab  10217  iseqf1olemqf  10219  iseqf1olemmo  10220  iseqf1olemqf1o  10221  iseqf1olemqk  10222  iseqf1olemjpcl  10223  iseqf1olemqpcl  10224  iseqf1olemfvp  10225  seq3f1olemqsumkj  10226  seq3f1olemqsumk  10227  seq3f1olemqsum  10228  seq3f1oleml  10231  seq3f1o  10232  seq3id3  10235  seq3id  10236  seq3homo  10238  seq3z  10239  seqfeq3  10240  fser0const  10244  ser3ge0  10245  exp3vallem  10249  exp3val  10250  expnnval  10251  expp1  10255  rpexpcl  10267  expaddzaplem  10291  leexp1a  10303  exple1  10304  subsq  10354  binom2  10358  binom3  10364  bernneq3  10369  expnbnd  10370  expcan  10418  nn0opthd  10423  faclbnd  10442  faclbnd6  10445  facubnd  10446  facavg  10447  bcval  10450  bccmpl  10455  bcval5  10464  bcpasc  10467  hashennnuni  10480  hashennn  10481  hashfiv01gt1  10483  fihasheqf1oi  10489  hashnncl  10497  fseq1hash  10502  fiprsshashgt1  10518  fimaxq  10528  fnfz0hash  10530  ffzo0hash  10532  zfz1isolemiso  10537  zfz1iso  10539  seq3coll  10540  shftfvalg  10545  ovshftex  10546  shftdm  10549  shftfib  10550  shftval  10552  shftval5  10556  shftf  10557  2shfti  10558  seq3shft  10565  crre  10584  rereb  10590  cjreim2  10631  cjap  10633  caucvgrelemrec  10706  caucvgrelemcau  10707  caucvgre  10708  cvg1nlemf  10710  cvg1nlemres  10712  uzin2  10714  rexuz3  10717  recvguniq  10722  sqrt0  10731  resqrexlemdecn  10739  resqrexlemlo  10740  resqrexlemcalc3  10743  resqrexlemnm  10745  resqrexlemcvg  10746  resqrexlemoverl  10748  resqrexlemglsq  10749  resqrexlemga  10750  resqrex  10753  sqrtgt0  10761  absrpclap  10788  absext  10790  absmul  10796  leabs  10801  nn0abscl  10812  ltabs  10814  abslt  10815  absle  10816  abssubap0  10817  abstri  10831  cau3lem  10841  caubnd2  10844  maxabsle  10931  maxabslemlub  10934  maxabslemval  10935  maxcl  10937  maxleastb  10941  maxltsup  10945  rexanre  10947  rexico  10948  zmaxcl  10951  2zsupmax  10952  fimaxre2  10953  minmax  10956  min2inf  10959  minabs  10962  minclpr  10963  mul0inf  10967  xrmaxiflemcl  10969  xrmaxifle  10970  xrmaxiflemab  10971  xrmaxiflemlub  10972  xrmaxiflemcom  10973  xrmaxiflemval  10974  xrltmaxsup  10981  xrmaxltsup  10982  xrmaxaddlem  10984  xrmaxadd  10985  xrnegiso  10986  xrminmax  10989  xrbdtri  11000  clim  11005  climi2  11012  climconst2  11015  climuni  11017  climmpt  11024  climshftlemg  11026  climres  11027  climcn1  11032  subcn2  11035  cn1lem  11038  climadd  11050  climmul  11051  climsub  11052  climle  11058  climsqz  11059  climsqz2  11060  clim2ser  11061  clim2ser2  11062  iserex  11063  isermulc2  11064  iserle  11066  iserge0  11067  climub  11068  climrecvg1n  11072  climcvg1nlem  11073  serf0  11076  sumeq2  11083  sumfct  11098  sumrbdclem  11100  fsum3cvg  11101  sumrbdc  11102  summodclem2a  11105  summodclem2  11106  summodc  11107  zsumdc  11108  isum  11109  fsum3  11111  sum0  11112  isumz  11113  fsumf1o  11114  isumss  11115  fisumss  11116  isumss2  11117  fsum3cvg2  11118  fsum3cvg3  11120  fsum3ser  11121  fsumcl2lem  11122  fsumcllem  11123  fsumadd  11130  fsumsplit  11131  sumsnf  11133  isumclim3  11147  isummulc2  11150  isumadd  11155  fsum2dlemstep  11158  fsum2d  11159  fisumcom2  11162  fsum0diaglem  11164  fsumrev  11167  fsumshft  11168  fisumrev2  11170  fsummulc2  11172  fsumconst  11178  modfsummod  11182  fsum00  11186  fsumabs  11189  telfsumo  11190  fsumparts  11194  fsumrelem  11195  iserabs  11199  cvgcmpub  11200  fsumiun  11201  binom1dif  11211  bcxmas  11213  isumshft  11214  isumlessdc  11220  divcnv  11221  trireciplem  11224  trirecip  11225  expcnvap0  11226  expcnvre  11227  expcnv  11228  explecnv  11229  geolim  11235  geolim2  11236  geo2sum  11238  geo2lim  11240  geoisum  11241  geoisumr  11242  geoisum1  11243  geoisum1c  11244  cvgratnnlemnexp  11248  cvgratnnlemseq  11250  cvgratz  11256  mertenslem2  11260  mertensabs  11261  eftvalcn  11277  ef0lem  11280  efcvgfsum  11287  ege2le3  11291  efcj  11293  efaddlem  11294  efadd  11295  eftlcvg  11307  eftlub  11310  efler  11319  eflegeo  11322  tanvalap  11329  tanclap  11330  tanval2ap  11334  tanval3ap  11335  tannegap  11349  sinadd  11357  cosadd  11358  eirrap  11396  dvdsval2  11408  dvdsdc  11413  moddvds  11414  zdvdsdc  11426  dvdscmul  11432  dvdsmulc  11433  dvdscmulr  11434  dvdsmulcr  11435  modmulconst  11437  dvdsadd  11448  dvdsadd2b  11452  dvdslelemd  11453  dvdsle  11454  dvdsabseq  11457  dvdseq  11458  divconjdvds  11459  dvds1  11463  fzo0dvdseq  11467  dvdsmod  11472  oddm1even  11484  mod2eq1n2dvds  11488  evennn02n  11491  evennn2n  11492  divalglemnn  11527  divalglemnqt  11529  divalglemeunn  11530  divalglemex  11531  divalglemeuneg  11532  divalg  11533  divalgmod  11536  modremain  11538  infssuzex  11554  gcdsupex  11558  gcdsupcl  11559  gcdval  11560  dvdslegcd  11565  gcdnncl  11568  gcdneg  11582  gcdaddm  11584  gcd1  11587  bezoutlemnewy  11596  bezoutlemmain  11598  bezoutlemex  11601  bezoutlemzz  11602  bezoutlemaz  11603  bezoutlembz  11604  bezoutlembi  11605  bezoutlemle  11608  bezoutlemsup  11609  gcdass  11615  gcdzeq  11622  dvdsmulgcd  11625  bezoutr1  11633  algrp1  11639  algcvga  11644  eucalgval2  11646  eucalgf  11648  eucalglt  11650  lcmval  11656  lcmledvds  11663  lcmneg  11667  lcmgcd  11671  lcmid  11673  coprmgcdb  11681  ncoprmgcdne1b  11682  mulgcddvds  11687  rpmulgcd2  11688  qredeq  11689  divgcdcoprm0  11694  divgcdcoprmex  11695  cncongr1  11696  cncongr2  11697  isprm2lem  11709  prmind2  11713  sqnprm  11728  isprm6  11737  prmdvdsexp  11738  prmfac1  11742  rpexp  11743  rpexp1i  11744  sqrt2irr  11752  pw2dvdslemn  11754  pw2dvdseulemle  11756  oddpwdclemxy  11758  oddpwdclemdc  11762  oddpwdc  11763  znege1  11767  sqrt2irraplemnn  11768  sqrt2irrap  11769  divnumden  11785  qden1elz  11794  phibndlem  11803  dfphi2  11807  phiprmpw  11809  crth  11811  phimullem  11812  oddennn  11816  evenennn  11817  ennnfonelemk  11824  ennnfonelemg  11827  ennnfonelemss  11834  ennnfoneleminc  11835  ennnfonelemkh  11836  ennnfonelemhf1o  11837  ennnfonelemex  11838  ennnfonelemhom  11839  ennnfonelemrnh  11840  ennnfonelemfun  11841  ennnfonelemf1  11842  ennnfonelemrn  11843  ennnfonelemdm  11844  ennnfonelemnn0  11846  exmidunben  11850  ctinfomlemom  11851  ctinfom  11852  ctinf  11854  ctiunctlemudc  11861  ctiunctlemf  11862  ctiunct  11864  unct  11865  isstruct2im  11880  isstruct2r  11881  setsvalg  11900  setsslid  11920  ressid2  11929  ressval2  11930  2strbasg  11971  2stropg  11972  2strop1g  11975  restval  12037  restid2  12040  eltg3i  12136  bastg  12141  topbas  12147  tgtop  12148  tgidm  12154  tgss2  12159  bastop2  12164  epttop  12170  iuncld  12195  clsss2  12209  isopn3i  12215  neiint  12225  neii2  12229  neissex  12245  restbasg  12248  tgrest  12249  resttopon  12251  ssrest  12262  restopn2  12263  lmfval  12272  cnpval  12278  lmcvg  12297  iscnp4  12298  cncnpi  12308  cnconst2  12313  cnrest  12315  cnrest2  12316  cnrest2r  12317  cnptopresti  12318  cnptoprest  12319  cnptoprest2  12320  lmss  12326  lmtopcnp  12330  txcnp  12351  upxp  12352  uptx  12354  txcn  12355  txlm  12359  cnmpt11  12363  cnmpt1t  12365  hmeores  12395  txswaphmeo  12401  psmetres2  12413  ismet2  12434  xmettri2  12441  xmetres2  12459  metres2  12461  blfvalps  12465  bldisj  12481  xblss2ps  12484  xblss2  12485  xblm  12497  blssps  12507  blss  12508  metss2lem  12577  metss2  12578  bdxmet  12581  bdbl  12583  metrest  12586  xmetxpbl  12588  xmettxlem  12589  xmettx  12590  metcnp3  12591  metcnp2  12593  metcnpi  12595  metcnpi2  12596  txmetcnp  12598  qtopbas  12602  tgioo  12626  addcncntoplem  12631  fsumcncntop  12636  rescncf  12648  cncfco  12658  cncfcncntop  12660  cncfmptid  12663  addccncf  12666  cdivcncfap  12667  negcncf  12668  mulcncflem  12670  mulcncf  12671  dedekindeulemuub  12675  dedekindeulemloc  12677  dedekindeulemlu  12679  dedekindeulemeu  12680  dedekindeu  12681  suplociccreex  12682  suplociccex  12683  dedekindicclemuub  12684  dedekindicclemloc  12686  dedekindicclemlu  12688  dedekindicclemeu  12689  dedekindicclemicc  12690  ivthinclemlopn  12694  ivthinclemlr  12695  ivthinclemuopn  12696  ivthinclemur  12697  ivthinclemloc  12699  ivthinc  12701  limccl  12708  ellimc3apf  12709  limcdifap  12711  limcmpted  12712  limcimolemlt  12713  limcimo  12714  cnplimcim  12716  cnplimclemle  12717  cnplimclemr  12718  cnlimcim  12720  limccnpcntop  12724  limccoap  12727  reldvg  12728  dvfvalap  12730  dvfgg  12737  dvidlemap  12740  dvcnp2cntop  12743  dvcjbr  12752  dvcj  12753  dvfre  12754  dvexp  12755  dvrecap  12757  dveflem  12766  dvef  12767  sin0pilem1  12773  sin0pilem2  12774  pilem3  12775  ptolemy  12816  coseq0q4123  12826  coseq0negpitopi  12828  bj-nnan  12844  bj-indind  13026  bj-omtrans  13050  pwtrufal  13088  pwle2  13089  pwf1oexmid  13090  subctctexmid  13092  nnsf  13095  peano4nninf  13096  nninfalllemn  13098  nninfalllem1  13099  nninfall  13100  nninfself  13105  nninfsellemeq  13106  nninfsellemqall  13107  nninfsellemeqinf  13108  nninfsel  13109  nninfomnilem  13110  nninffeq  13112  sbthom  13117  qdencn  13118  refeq  13119  isomninnlem  13121  trilpolemclim  13125  trilpolemcl  13126  trilpolemisumle  13127  trilpolemeq1  13129  trilpolemlt1  13130  trilpolemres  13131
  Copyright terms: Public domain W3C validator