Theorem elinel2 3632

Description: Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
elinel2	|- ( A e. ( B i^i C ) -> A e. C )

Proof of Theorem elinel2

Step	Hyp	Ref	Expression
1		elin 3629	. 2 |- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )
2	1	simprbi 470	1 |- ( A e. ( B i^i C ) -> A e. C )

Syntax hints:   -> wi 4   e. wcel 1898   i^i cin 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423

This theorem is referenced by:  xrge0tsmsd  28599  heicant  32021  fiinfi  36223  disjinfi  37522  inmap  37547  iocopn  37706  icoopn  37711  islpcn  37805  lptre2pt  37806  limcresiooub  37809  limcresioolb  37810  limclner  37818  icccncfext  37851  stoweidlem39  38001  stoweidlem50  38012  stoweidlem57  38019  fourierdlem32  38103  fourierdlem33  38104  fourierdlem48  38119  fourierdlem49  38120  fourierdlem71  38142  fourierdlem80  38151  qndenserrnbllem  38264  sge0rnre  38309  sge0z  38320  sge0tsms  38325  sge0cl  38326  sge0f1o  38327  sge0fsum  38332  sge0sup  38336  sge0rnbnd  38338  sge0ltfirp  38345  sge0resplit  38351  sge0le  38352  sge0split  38354  sge0iunmptlemre  38360  sge0ltfirpmpt2  38371  sge0isum  38372  sge0xaddlem1  38378  sge0xaddlem2  38379  sge0pnffsumgt  38387  sge0gtfsumgt  38388  sge0uzfsumgt  38389  sge0seq  38391  meadjiunlem  38408  caragendifcl  38443  omeiunltfirp  38448  carageniuncllem2  38451  caratheodorylem2  38456  hspmbllem2  38556  uhgrspansubgrlem  39508  rnghmsubcsetclem2  40347  rhmsubcsetclem2  40393  rhmsubcrngclem2  40399