Theorem elind 3687

Description: Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
elind.1
elind.2

Assertion

Ref	Expression
elind

Proof of Theorem elind

Step	Hyp	Ref	Expression
1		elind.1	. 2
2		elind.2	. 2
3		elin 3686	. 2
4	1, 2, 3	sylanbrc 664	1

Syntax hints:  ->wi 4  e.wcel 1818  i^icin 3474

This theorem is referenced by:  tfrlem5  7068  uniinqs  7410  unifpw  7843  f1opwfi  7844  fissuni  7845  fipreima  7846  elfir  7895  inelfi  7898  cantnfcl  8107  cantnfclOLD  8137  tskwe  8352  infpwfidom  8430  infpwfien  8464  ackbij2lem1  8620  ackbij1lem3  8623  ackbij1lem4  8624  ackbij1lem6  8626  ackbij1lem11  8631  fin23lem24  8723  isfin1-3  8787  fpwwe2lem12  9040  fpwwe  9045  canthnumlem  9047  fz1isolem  12510  strfv2d  14664  submre  15002  submrc  15025  isacs2  15050  coffth  15305  catcoppccl  15435  catcfuccl  15436  catcxpccl  15476  isdrs2  15568  fpwipodrs  15794  sylow2a  16639  lsmmod  16693  lsmdisj  16699  lsmdisj2  16700  subgdisj1  16709  frgpnabllem1  16877  dmdprdd  17030  dprdfeq0  17062  dprdfeq0OLD  17069  dprdres  17075  dprddisj2  17087  dprddisj2OLD  17088  dprd2da  17091  dmdprdsplit2lem  17094  ablfacrp  17117  pgpfac1lem3a  17127  pgpfac1lem3  17128  pgpfaclem1  17132  aspval  17977  mplind  18167  zringlpirlem1  18509  zringlpirlem3  18511  zlpirlem1  18514  zlpirlem3  18516  pmatcoe1fsupp  19202  baspartn  19455  bastg  19467  clsval2  19551  isopn3  19567  restbas  19659  lmss  19799  cmpcovf  19891  discmp  19898  cmpsublem  19899  cmpsub  19900  iscon2  19915  conclo  19916  llynlly  19978  restnlly  19983  restlly  19984  islly2  19985  llyrest  19986  nllyrest  19987  llyidm  19989  nllyidm  19990  hausllycmp  19995  cldllycmp  19996  lly1stc  19997  dislly  19998  llycmpkgen2  20051  1stckgenlem  20054  txlly  20137  txnlly  20138  txtube  20141  txcmplem1  20142  txcmplem2  20143  xkococnlem  20160  basqtop  20212  tgqtop  20213  infil  20364  fmfnfmlem4  20458  hauspwpwf1  20488  tgpconcompss  20612  ustfilxp  20715  metrest  21027  tgioo  21301  zdis  21321  icccmplem1  21327  icccmplem2  21328  reconnlem2  21332  xrge0tsms  21339  cnheibor  21455  cnllycmp  21456  cphsqrtcl  21631  cmetcaulem  21727  ovollb2lem  21899  ovolctb  21901  ovolshftlem1  21920  ovolscalem1  21924  ovolicc1  21927  ioombl1lem1  21968  ioorf  21982  ioorcl  21986  dyadf  22000  vitalilem2  22018  vitali  22022  i1faddlem  22100  dvres2lem  22314  dvaddbr  22341  dvmulbr  22342  lhop1lem  22414  lhop  22417  dvcnvrelem2  22419  ig1peu  22572  tayl0  22757  rlimcnp2  23296  xrlimcnp  23298  ppisval  23377  ppisval2  23378  ppinprm  23426  chtnprm  23428  2sqlem7  23645  chebbnd1lem1  23654  footex  24095  foot  24096  footne  24097  perprag  24100  colperpexlem3  24106  mideulem2  24108  lnopp2hpgb  24132  lmieu  24150  lmimid  24159  hypcgrlem1  24164  hypcgrlem2  24165  f1otrg  24174  eengtrkg  24288  mndomgmid  25344  shuni  26218  5oalem1  26572  5oalem2  26573  5oalem4  26575  5oalem5  26576  3oalem2  26581  pjclem4  27118  pj3si  27126  xrge0tsmsd  27775  cmpcref  27853  cmppcmp  27861  dispcmp  27862  prsdm  27896  prsrn  27897  pnfneige0  27933  qqhucn  27973  gsumesum  28067  esumcst  28071  sigainb  28136  eulerpartlemgh  28317  eulerpartlemgs2  28319  eulerpartlemn  28320  sseqmw  28330  sseqf  28331  sseqp1  28334  fibp1  28340  cnllyscon  28690  rellyscon  28696  cvmsss2  28719  cvmcov2  28720  cvmopnlem  28723  mclsind  28930  blbnd  30283  ssbnd  30284  heiborlem1  30307  heiborlem8  30314  heibor  30317  elrfi  30626  elrfirn  30627  fnwe2lem2  30997  dfac11  31008  kelac1  31009  kelac2lem  31010  dfac21  31012  islssfgi  31018  filnm  31036  lpirlnr  31066  hbtlem6  31078  hbt  31079  cntzsdrg  31151  iocinico  31179  isprm7  31192  iooabslt  31532  iocopn  31560  icoopn  31565  limciccioolb  31627  limcicciooub  31643  islpcn  31645  limcresioolb  31649  limcleqr  31650  ioccncflimc  31688  icccncfext  31690  icocncflimc  31692  cncfiooicclem1  31696  itgiccshift  31779  itgperiod  31780  itgsbtaddcnst  31781  stoweidlem57  31839  fourierdlem20  31909  fourierdlem32  31921  fourierdlem33  31922  fourierdlem48  31937  fourierdlem49  31938  fourierdlem62  31951  fourierdlem71  31960  fouriersw  32014  zrinitorngc  32808  zrtermorngc  32809  zrzeroorngc  32810  irinitoringc  32877  zrtermoringc  32878  zrninitoringc  32879  nzerooringczr  32880  bnj1379  33889  bnj1177  34062  pmodlem1  35570  pclfinN  35624  mapdunirnN  37377  hdmaprnlem9N  37587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482