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  274  ibar  297  pm3.42  328  pm3.4  329  anim12  339  simpl2im  381  sylancom  414  adantll  465  adantrl  467  adantlll  469  adantlrl  471  adantrll  473  adantrrl  475  simpllr  506  simplrr  508  simprlr  510  simprrr  512  anabs7  546  jcab  575  pm4.38  577  pm5.21  667  ioran  724  pm3.14  725  ordi  788  pm4.39  794  pm5.16  796  pm5.54dc  886  intnan  897  intnand  899  dcan  901  bimsc1  930  niabn  934  simp1r  989  simp2r  991  simp3r  993  3anandirs  1309  bilukdc  1357  19.26  1440  exsimpr  1580  19.40  1593  cbvexh  1711  sbequilem  1792  spsbe  1796  cbvexdh  1876  euan  2031  moan  2044  datisi  2085  fresison  2093  rexex  2454  r19.26  2533  r19.29an  2549  r19.40  2560  cbvraldva2  2633  cbvrexdva2  2634  gencbvex  2704  rspct  2754  rspcimdv  2762  rspcimedv  2763  rr19.28v  2796  elrab3t  2810  reu6  2844  rmob  2971  csbiebt  3007  rabssab  3152  ssddif  3278  difin  3281  difrab  3318  dcun  3441  eqifdc  3474  ifmdc  3477  preqsn  3670  opprc2  3696  dfnfc2  3722  intmin4  3767  sndisj  3893  undifexmid  4085  exmid01  4089  pwntru  4090  exmidn0m  4092  exmidsssn  4093  exmidsssnc  4094  exmidundif  4097  exmidundifim  4098  exss  4117  euotd  4144  frirrg  4240  suctr  4311  abnexg  4335  ordtri2or2exmid  4454  wetriext  4459  reg3exmidlemwe  4461  tfisi  4469  peano2  4477  omsinds  4503  nnpredcl  4504  relop  4657  releldm  4742  relelrn  4743  resiexg  4832  trin2  4898  xpmlem  4927  unielrel  5034  relcoi2  5037  iota2df  5080  iota2  5082  funopab4  5128  fun11uni  5161  imadiflem  5170  imain  5173  fneq12  5184  f1ssr  5303  fvelrnb  5435  ssimaex  5448  fvmpt2d  5473  fvmptdf  5474  dffo3  5533  ffvresb  5549  fmptco  5552  funfvima3  5617  f1imass  5641  fliftf  5666  fliftval  5667  riota2df  5716  riota5f  5720  acexmidlemcase  5735  ovprc2  5774  eloprabga  5824  eqfnov2  5844  ovmpodxf  5862  ofvalg  5957  offval2  5963  ofrfval2  5964  caofinvl  5970  2ndrn  6047  1st2ndbr  6048  cnvf1o  6088  f1o2ndf1  6091  mpoxopoveq  6103  dftpos4  6126  tpostpos  6127  tposf12  6132  dfsmo2  6150  smores  6155  tfrlem1  6171  tfrlem3ag  6172  tfrlem3a  6173  tfrlemisucaccv  6188  tfrlemi1  6195  tfrexlem  6197  tfr1onlem3ag  6200  tfr1onlemsucaccv  6204  tfr1onlembxssdm  6206  tfr1onlembfn  6207  tfr1onlemaccex  6211  tfr1onlemres  6212  tfri1dALT  6214  tfrcllemsucaccv  6217  tfrcllembxssdm  6219  tfrcllembfn  6220  tfrcllemaccex  6224  tfrcllemres  6225  tfrcl  6227  rdgivallem  6244  rdgon  6249  frecabex  6261  frecabcl  6262  frectfr  6263  frecrdg  6271  oawordi  6331  nntri3  6359  nntr2  6365  dcdifsnid  6366  nnaordi  6370  nnaordex  6389  nnawordex  6390  nnm00  6391  ersymb  6409  ertr  6410  erref  6415  iserd  6421  swoer  6423  erth  6439  iinerm  6467  erinxp  6469  ecinxp  6470  qsel  6472  qliftel  6475  qliftfun  6477  fvdiagfn  6553  ixpssmapg  6588  resixp  6593  mptelixpg  6594  dom3  6636  ssdomg  6638  cnven  6668  xpen  6705  xpmapenlem  6709  ssenen  6711  phplem4dom  6722  phpm  6725  phpelm  6726  fidifsnen  6730  fin0  6745  fin0or  6746  isinfinf  6757  tridc  6759  fimax2gtrilemstep  6760  fimax2gtri  6761  finexdc  6762  en2eqpr  6767  fientri3  6769  unsnfidcex  6774  unsnfidcel  6775  unfidisj  6776  undifdcss  6777  undifdc  6778  unfiin  6780  fiintim  6783  fnfi  6791  relcnvfi  6795  f1dmvrnfibi  6798  iunfidisj  6800  f1finf1o  6801  fidcenumlemrks  6807  fidcenumlemr  6809  fidcenum  6810  fival  6824  elfi2  6826  ssfii  6828  fiss  6831  suplubti  6853  suplub2ti  6854  supelti  6855  supisolem  6861  supisoex  6862  infglbti  6878  ordiso2  6886  djuss  6921  updjudhcoinlf  6931  updjudhcoinrg  6932  updjud  6933  djudom  6944  omp1eomlem  6945  difinfsnlem  6950  difinfsn  6951  difinfinf  6952  ctm  6960  ctssdclemn0  6961  ctssdccl  6962  ctssdc  6964  enumctlemm  6965  enumct  6966  enomnilem  6976  finomni  6978  exmidomni  6980  fodjuomnilemdc  6982  fodjuomnilemres  6986  nnnninf  6989  ctssexmid  6990  ismkvnex  6995  mkvprop  6998  fodjumkvlemres  6999  en2eleq  7015  en2other2  7016  exmidfodomrlemeldju  7019  exmidfodomrlemreseldju  7020  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  exmidaclem  7028  dju1en  7033  djudomr  7040  dmaddpqlem  7149  nqpi  7150  mulcanenq  7157  ltaddnq  7179  ltexnqq  7180  prarloclemarch2  7191  ltrnqg  7192  ltnnnq  7195  enq0sym  7204  nqnq0pi  7210  nq0nn  7214  mulcanenq0ec  7217  addnq0mo  7219  mulnq0mo  7220  addnnnq0  7221  prloc  7263  prarloclemlt  7265  prarloclemlo  7266  ltdfpr  7278  genplt2i  7282  genpml  7289  genpmu  7290  addnqprllem  7299  addnqprulem  7300  addnqprl  7301  addnqpru  7302  nqprloc  7317  appdivnq  7335  appdiv0nq  7336  mulnqprl  7340  mulnqpru  7341  distrlem1prl  7354  distrlem1pru  7355  ltprordil  7361  1idprl  7362  1idpru  7363  ltexprlemrl  7382  ltexprlemru  7384  ltexpri  7385  addcanprleml  7386  addcanprlemu  7387  recexprlem1ssl  7405  recexpr  7410  aptiprlemu  7412  archpr  7415  cauappcvgprlemopl  7418  cauappcvgprlemdisj  7423  cauappcvgprlemloc  7424  cauappcvgprlemladdfu  7426  cauappcvgprlemladdfl  7427  cauappcvgprlemladdru  7428  cauappcvgprlemladdrl  7429  caucvgprlemm  7440  caucvgprlemopl  7441  caucvgprlemloc  7447  caucvgprlemladdfu  7449  caucvgprlemladdrl  7450  caucvgprlemlim  7453  caucvgprprlemval  7460  caucvgprprlemml  7466  caucvgprprlemopl  7469  caucvgprprlemopu  7471  caucvgprprlemloc  7475  caucvgprprlemexbt  7478  caucvgprprlemexb  7479  caucvgprprlemaddq  7480  caucvgprprlemlim  7483  suplocexprlemru  7491  suplocexprlemloc  7493  suplocexprlemub  7495  suplocexprlemlub  7496  addsrmo  7515  mulsrmo  7516  addsrpr  7517  mulsrpr  7518  0idsr  7539  1idsr  7540  recexsrlem  7546  addgt0sr  7547  srpospr  7555  prsradd  7558  prsrlt  7559  caucvgsrlemfv  7563  caucvgsrlemgt1  7567  caucvgsrlemoffval  7568  caucvgsrlemoffcau  7570  caucvgsrlemoffres  7572  mappsrprg  7576  map2psrprg  7577  suplocsrlemb  7578  suplocsrlem  7580  suplocsr  7581  rereceu  7661  axarch  7663  nntopi  7666  axcaucvglemval  7669  axpre-suploclemres  7673  axpre-suploc  7674  axsuploc  7801  muladd11r  7882  cnegexlem1  7901  cnegex  7904  negeu  7917  pncan  7932  pncan3  7934  npcan  7935  addid0  8099  negf1o  8108  mulneg1  8121  lelttrdi  8152  ltnegcon2  8190  add20  8200  subge0  8201  lesub0  8205  reapval  8301  recexre  8303  apreap  8312  ltmul1a  8316  reapneg  8322  cru  8327  apsym  8331  apcotr  8332  apadd1  8333  apneg  8336  mulext1  8337  apti  8347  gt0ap0  8351  ap0gt0  8364  subap0  8367  recexap  8374  divmulassap  8415  divmulasscomap  8416  rerecclap  8450  recgt0  8565  prodgt0gt0  8566  lemul1a  8573  lemul12a  8577  lt2msq  8601  ltrec1  8603  recreclt  8615  negiso  8670  sup3exmid  8672  creui  8675  cju  8676  avglt2  8910  un0addcl  8961  nn0ge2m1nn  8988  nn0nndivcl  8990  elnn0z  9018  peano2z  9041  elz2  9073  suprzclex  9100  peano5uzti  9110  zindd  9120  btwnapz  9132  eluzadd  9303  nn0pzuz  9331  supinfneg  9339  infsupneg  9340  eluz2b2  9346  eqreznegel  9355  nn0ge2m1nnALT  9359  divfnzn  9362  qmulz  9364  qapne  9380  qreccl  9383  cnref1o  9389  ge0p1rp  9421  xrltso  9522  npnflt  9538  nmnfgt  9541  z2ge  9549  xltnegi  9558  xaddval  9568  xaddcom  9584  xnegdi  9591  xaddass  9592  xpncan  9594  xleadd1a  9596  xltadd1  9599  xlt2add  9603  xsubge0  9604  xposdif  9605  xlesubadd  9606  xleaddadd  9610  ixxssixx  9625  lincmb01cmp  9726  iccf1o  9727  zltaddlt1le  9729  fztri3or  9759  fzdcel  9760  fznlem  9761  fzn  9762  uzsubsubfz  9767  fzsplit2  9770  fzopth  9781  fzdifsuc  9801  fzrev2i  9806  elfz1b  9810  fzneuz  9821  fzrevral  9825  ige2m1fz  9830  elfz0ubfz0  9842  elfz0fzfz0  9843  4fvwrd4  9857  2ffzeq  9858  fzospliti  9893  fzosplit  9894  fzo1fzo0n0  9900  fzonmapblen  9904  fzoaddel  9909  fzosubel  9911  fzosubel3  9913  elfzodifsumelfzo  9918  elfzom1elp1fzo  9919  elfzom1p1elfzo  9931  elfzonelfzo  9947  peano2fzor  9949  exfzdc  9957  fvinim0ffz  9958  qtri3or  9960  exbtwnzlemstep  9965  rebtwn2zlemstep  9970  qbtwnxr  9975  apbtwnz  9987  flqge  9995  flqltnz  10000  flqaddz  10010  btwnzge0  10013  flltdivnn0lt  10017  intfracq  10033  flqdiv  10034  modqid0  10063  q0mod  10068  q1mod  10069  modqmuladdim  10080  modqmuladdnn0  10081  q2txmodxeq0  10097  q2submod  10098  modifeq2int  10099  modqsubdir  10106  modsumfzodifsn  10109  addmodlteq  10111  frec2uzzd  10113  frec2uzuzd  10115  frec2uzrand  10118  frec2uzf1od  10119  frecuzrdgrrn  10121  frec2uzrdg  10122  frecuzrdgtcl  10125  frecuzrdgsuc  10127  frecuzrdgg  10129  frecuzrdgdomlem  10130  frecuzrdgfunlem  10132  frecuzrdgsuctlem  10136  frecfzennn  10139  uzsinds  10155  seq3val  10171  seqvalcd  10172  seq3clss  10180  seq3feq2  10183  seq3feq  10185  ser3mono  10191  seq3split  10192  iseqf1olemkle  10197  iseqf1olemklt  10198  iseqf1olemqcl  10199  iseqf1olemnab  10201  iseqf1olemab  10202  iseqf1olemqf  10204  iseqf1olemmo  10205  iseqf1olemqf1o  10206  iseqf1olemqk  10207  iseqf1olemjpcl  10208  iseqf1olemqpcl  10209  iseqf1olemfvp  10210  seq3f1olemqsumkj  10211  seq3f1olemqsumk  10212  seq3f1olemqsum  10213  seq3f1oleml  10216  seq3f1o  10217  seq3id3  10220  seq3id  10221  seq3homo  10223  seq3z  10224  seqfeq3  10225  fser0const  10229  ser3ge0  10230  exp3vallem  10234  exp3val  10235  expnnval  10236  expp1  10240  rpexpcl  10252  expaddzaplem  10276  leexp1a  10288  exple1  10289  subsq  10339  binom2  10343  binom3  10349  bernneq3  10354  expnbnd  10355  expcan  10403  nn0opthd  10408  faclbnd  10427  faclbnd6  10430  facubnd  10431  facavg  10432  bcval  10435  bccmpl  10440  bcval5  10449  bcpasc  10452  hashennnuni  10465  hashennn  10466  hashfiv01gt1  10468  fihasheqf1oi  10474  hashnncl  10482  fseq1hash  10487  fiprsshashgt1  10503  fimaxq  10513  fnfz0hash  10515  ffzo0hash  10517  zfz1isolemiso  10522  zfz1iso  10524  seq3coll  10525  shftfvalg  10530  ovshftex  10531  shftdm  10534  shftfib  10535  shftval  10537  shftval5  10541  shftf  10542  2shfti  10543  seq3shft  10550  crre  10569  rereb  10575  cjreim2  10616  cjap  10618  caucvgrelemrec  10691  caucvgrelemcau  10692  caucvgre  10693  cvg1nlemf  10695  cvg1nlemres  10697  uzin2  10699  rexuz3  10702  recvguniq  10707  sqrt0  10716  resqrexlemdecn  10724  resqrexlemlo  10725  resqrexlemcalc3  10728  resqrexlemnm  10730  resqrexlemcvg  10731  resqrexlemoverl  10733  resqrexlemglsq  10734  resqrexlemga  10735  resqrex  10738  sqrtgt0  10746  absrpclap  10773  absext  10775  absmul  10781  leabs  10786  nn0abscl  10797  ltabs  10799  abslt  10800  absle  10801  abssubap0  10802  abstri  10816  cau3lem  10826  caubnd2  10829  maxabsle  10916  maxabslemlub  10919  maxabslemval  10920  maxcl  10922  maxleastb  10926  maxltsup  10930  rexanre  10932  rexico  10933  zmaxcl  10936  2zsupmax  10937  fimaxre2  10938  minmax  10941  min2inf  10944  minabs  10947  minclpr  10948  mul0inf  10952  xrmaxiflemcl  10954  xrmaxifle  10955  xrmaxiflemab  10956  xrmaxiflemlub  10957  xrmaxiflemcom  10958  xrmaxiflemval  10959  xrltmaxsup  10966  xrmaxltsup  10967  xrmaxaddlem  10969  xrmaxadd  10970  xrnegiso  10971  xrminmax  10974  xrbdtri  10985  clim  10990  climi2  10997  climconst2  11000  climuni  11002  climmpt  11009  climshftlemg  11011  climres  11012  climcn1  11017  subcn2  11020  cn1lem  11023  climadd  11035  climmul  11036  climsub  11037  climle  11043  climsqz  11044  climsqz2  11045  clim2ser  11046  clim2ser2  11047  iserex  11048  isermulc2  11049  iserle  11051  iserge0  11052  climub  11053  climrecvg1n  11057  climcvg1nlem  11058  serf0  11061  sumeq2  11068  sumfct  11083  sumrbdclem  11085  fsum3cvg  11086  sumrbdc  11087  summodclem2a  11090  summodclem2  11091  summodc  11092  zsumdc  11093  isum  11094  fsum3  11096  sum0  11097  isumz  11098  fsumf1o  11099  isumss  11100  fisumss  11101  isumss2  11102  fsum3cvg2  11103  fsum3cvg3  11105  fsum3ser  11106  fsumcl2lem  11107  fsumcllem  11108  fsumadd  11115  fsumsplit  11116  sumsnf  11118  isumclim3  11132  isummulc2  11135  isumadd  11140  fsum2dlemstep  11143  fsum2d  11144  fisumcom2  11147  fsum0diaglem  11149  fsumrev  11152  fsumshft  11153  fisumrev2  11155  fsummulc2  11157  fsumconst  11163  modfsummod  11167  fsum00  11171  fsumabs  11174  telfsumo  11175  fsumparts  11179  fsumrelem  11180  iserabs  11184  cvgcmpub  11185  fsumiun  11186  binom1dif  11196  bcxmas  11198  isumshft  11199  isumlessdc  11205  divcnv  11206  trireciplem  11209  trirecip  11210  expcnvap0  11211  expcnvre  11212  expcnv  11213  explecnv  11214  geolim  11220  geolim2  11221  geo2sum  11223  geo2lim  11225  geoisum  11226  geoisumr  11227  geoisum1  11228  geoisum1c  11229  cvgratnnlemnexp  11233  cvgratnnlemseq  11235  cvgratz  11241  mertenslem2  11245  mertensabs  11246  eftvalcn  11262  ef0lem  11265  efcvgfsum  11272  ege2le3  11276  efcj  11278  efaddlem  11279  efadd  11280  eftlcvg  11292  eftlub  11295  efler  11304  eflegeo  11307  tanvalap  11314  tanclap  11315  tanval2ap  11319  tanval3ap  11320  tannegap  11334  sinadd  11342  cosadd  11343  eirrap  11380  dvdsval2  11392  dvdsdc  11397  moddvds  11398  zdvdsdc  11410  dvdscmul  11416  dvdsmulc  11417  dvdscmulr  11418  dvdsmulcr  11419  modmulconst  11421  dvdsadd  11432  dvdsadd2b  11436  dvdslelemd  11437  dvdsle  11438  dvdsabseq  11441  dvdseq  11442  divconjdvds  11443  dvds1  11447  fzo0dvdseq  11451  dvdsmod  11456  oddm1even  11468  mod2eq1n2dvds  11472  evennn02n  11475  evennn2n  11476  divalglemnn  11511  divalglemnqt  11513  divalglemeunn  11514  divalglemex  11515  divalglemeuneg  11516  divalg  11517  divalgmod  11520  modremain  11522  infssuzex  11538  gcdsupex  11542  gcdsupcl  11543  gcdval  11544  dvdslegcd  11549  gcdnncl  11552  gcdneg  11566  gcdaddm  11568  gcd1  11571  bezoutlemnewy  11580  bezoutlemmain  11582  bezoutlemex  11585  bezoutlemzz  11586  bezoutlemaz  11587  bezoutlembz  11588  bezoutlembi  11589  bezoutlemle  11592  bezoutlemsup  11593  gcdass  11599  gcdzeq  11606  dvdsmulgcd  11609  bezoutr1  11617  algrp1  11623  algcvga  11628  eucalgval2  11630  eucalgf  11632  eucalglt  11634  lcmval  11640  lcmledvds  11647  lcmneg  11651  lcmgcd  11655  lcmid  11657  coprmgcdb  11665  ncoprmgcdne1b  11666  mulgcddvds  11671  rpmulgcd2  11672  qredeq  11673  divgcdcoprm0  11678  divgcdcoprmex  11679  cncongr1  11680  cncongr2  11681  isprm2lem  11693  prmind2  11697  sqnprm  11712  isprm6  11721  prmdvdsexp  11722  prmfac1  11726  rpexp  11727  rpexp1i  11728  sqrt2irr  11736  pw2dvdslemn  11738  pw2dvdseulemle  11740  oddpwdclemxy  11742  oddpwdclemdc  11746  oddpwdc  11747  znege1  11751  sqrt2irraplemnn  11752  sqrt2irrap  11753  divnumden  11769  qden1elz  11778  phibndlem  11787  dfphi2  11791  phiprmpw  11793  crth  11795  phimullem  11796  oddennn  11800  evenennn  11801  ennnfonelemk  11808  ennnfonelemg  11811  ennnfonelemss  11818  ennnfoneleminc  11819  ennnfonelemkh  11820  ennnfonelemhf1o  11821  ennnfonelemex  11822  ennnfonelemhom  11823  ennnfonelemrnh  11824  ennnfonelemfun  11825  ennnfonelemf1  11826  ennnfonelemrn  11827  ennnfonelemdm  11828  ennnfonelemnn0  11830  exmidunben  11834  ctinfomlemom  11835  ctinfom  11836  ctinf  11838  ctiunctlemudc  11845  ctiunctlemf  11846  ctiunct  11848  unct  11849  isstruct2im  11864  isstruct2r  11865  setsvalg  11884  setsslid  11904  ressid2  11913  ressval2  11914  2strbasg  11955  2stropg  11956  2strop1g  11959  restval  12021  restid2  12024  eltg3i  12120  bastg  12125  topbas  12131  tgtop  12132  tgidm  12138  tgss2  12143  bastop2  12148  epttop  12154  iuncld  12179  clsss2  12193  isopn3i  12199  neiint  12209  neii2  12213  neissex  12229  restbasg  12232  tgrest  12233  resttopon  12235  ssrest  12246  restopn2  12247  lmfval  12256  cnpval  12262  lmcvg  12281  iscnp4  12282  cncnpi  12292  cnconst2  12297  cnrest  12299  cnrest2  12300  cnrest2r  12301  cnptopresti  12302  cnptoprest  12303  cnptoprest2  12304  lmss  12310  lmtopcnp  12314  txcnp  12335  upxp  12336  uptx  12338  txcn  12339  txlm  12343  cnmpt11  12347  cnmpt1t  12349  hmeores  12379  txswaphmeo  12385  psmetres2  12397  ismet2  12418  xmettri2  12425  xmetres2  12443  metres2  12445  blfvalps  12449  bldisj  12465  xblss2ps  12468  xblss2  12469  xblm  12481  blssps  12491  blss  12492  metss2lem  12561  metss2  12562  bdxmet  12565  bdbl  12567  metrest  12570  xmetxpbl  12572  xmettxlem  12573  xmettx  12574  metcnp3  12575  metcnp2  12577  metcnpi  12579  metcnpi2  12580  txmetcnp  12582  qtopbas  12586  tgioo  12610  addcncntoplem  12615  fsumcncntop  12620  rescncf  12632  cncfco  12642  cncfcncntop  12644  cncfmptid  12647  addccncf  12650  cdivcncfap  12651  negcncf  12652  mulcncflem  12654  mulcncf  12655  dedekindeulemuub  12659  dedekindeulemloc  12661  dedekindeulemlu  12663  dedekindeulemeu  12664  dedekindeu  12665  limccl  12671  ellimc3apf  12672  limcdifap  12674  limcmpted  12675  limcimolemlt  12676  limcimo  12677  cnplimcim  12679  cnplimclemle  12680  cnplimclemr  12681  cnlimcim  12683  limccnpcntop  12687  limccoap  12690  reldvg  12691  dvfvalap  12693  dvfgg  12700  dvidlemap  12703  dvcnp2cntop  12706  dvcjbr  12715  dvcj  12716  dvfre  12717  dvexp  12718  dvrecap  12720  dveflem  12729  dvef  12730  bj-nnan  12750  bj-indind  12932  bj-omtrans  12956  pwtrufal  12994  pwle2  12995  pwf1oexmid  12996  subctctexmid  12998  nnsf  13001  peano4nninf  13002  nninfalllemn  13004  nninfalllem1  13005  nninfall  13006  nninfself  13011  nninfsellemeq  13012  nninfsellemqall  13013  nninfsellemeqinf  13014  nninfsel  13015  nninfomnilem  13016  nninffeq  13018  sbthom  13023  qdencn  13024  refeq  13025  isomninnlem  13027  trilpolemclim  13031  trilpolemcl  13032  trilpolemisumle  13033  trilpolemeq1  13035  trilpolemlt1  13036  trilpolemres  13037
  Copyright terms: Public domain W3C validator