Theorem elinel2 3762

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

Assertion

Ref	Expression
elinel2	⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)

Proof of Theorem elinel2

Step	Hyp	Ref	Expression
1		elin 3758	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2	1	simprbi 479	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 1977   ∩ cin 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547

This theorem is referenced by:  elin2d  3765  eldmeldmressn  5360  onfr  5680  ncvsge0  22761  itg2cnlem2  23335  xrge0tsmsd  29116  heicant  32614  fiinfi  36897  restuni3  38333  disjinfi  38375  inmap  38396  iocopn  38593  icoopn  38598  icomnfinre  38626  islpcn  38706  lptre2pt  38707  limcresiooub  38709  limcresioolb  38710  limclner  38718  icccncfext  38773  stoweidlem39  38932  stoweidlem50  38943  stoweidlem57  38950  fourierdlem32  39032  fourierdlem33  39033  fourierdlem48  39047  fourierdlem49  39048  fourierdlem71  39070  fourierdlem80  39079  qndenserrnbllem  39190  sge0rnre  39257  sge0z  39268  sge0tsms  39273  sge0cl  39274  sge0f1o  39275  sge0fsum  39280  sge0sup  39284  sge0rnbnd  39286  sge0ltfirp  39293  sge0resplit  39299  sge0le  39300  sge0split  39302  sge0iunmptlemre  39308  sge0ltfirpmpt2  39319  sge0isum  39320  sge0xaddlem1  39326  sge0xaddlem2  39327  sge0pnffsumgt  39335  sge0gtfsumgt  39336  sge0uzfsumgt  39337  sge0seq  39339  sge0reuz  39340  meadjiunlem  39358  caragendifcl  39404  omeiunltfirp  39409  carageniuncllem2  39412  caratheodorylem2  39417  hspmbllem2  39517  pimiooltgt  39598  pimdecfgtioc  39602  pimincfltioc  39603  pimdecfgtioo  39604  pimincfltioo  39605  sssmf  39625  smfaddlem1  39649  smfaddlem2  39650  smfadd  39651  mbfpsssmf  39669  smfmullem4  39679  smfmul  39680  smfdiv  39682  fmtno4prm  40025  uhgrspansubgrlem  40514  rnghmsubcsetclem2  41768  rhmsubcsetclem2  41814  rhmsubcrngclem2  41820