Theorem elinel1 3799

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

Assertion

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

Proof of Theorem elinel1

Step	Hyp	Ref	Expression
1		elin 3796	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2	1	simplbi 476	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 1990   ∩ cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  elin1d  3802  inss1  3833  predel  5697  prmreclem2  15621  txkgen  21455  ncvsge0  22953  dchrisum0re  25202  uhgrspansubgrlem  26182  disjin  29399  xrge0tsmsd  29785  eulerpartgbij  30434  fiinfi  37878  gneispace  38432  elpwinss  39216  restuni3  39301  nel1nelin  39337  disjinfi  39380  inmap  39401  iocopn  39746  icoopn  39751  icomnfinre  39779  uzinico  39787  islpcn  39871  lptre2pt  39872  limcresiooub  39874  limcresioolb  39875  limsupmnflem  39952  limsupresxr  39998  liminfresxr  39999  liminfvalxr  40015  liminf0  40025  icccncfext  40100  stoweidlem39  40256  stoweidlem50  40267  stoweidlem57  40274  fourierdlem32  40356  fourierdlem33  40357  fourierdlem48  40371  fourierdlem49  40372  fourierdlem71  40394  sge0rnre  40581  sge00  40593  sge0tsms  40597  sge0cl  40598  sge0fsum  40604  sge0sup  40608  sge0less  40609  sge0gerp  40612  sge0resplit  40623  sge0split  40626  sge0iunmptlemre  40632  caragendifcl  40728  hoiqssbllem3  40838  hspmbllem2  40841  pimiooltgt  40921  pimdecfgtioc  40925  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  sssmf  40947  smfaddlem1  40971  smfaddlem2  40972  smfadd  40973  mbfpsssmf  40991  smfmul  41002  smfdiv  41004  smfsuplem1  41017  smfliminflem  41036  fmtno4prm  41487  rngcid  41979  ringcid  42025  rhmsubclem3  42088  rhmsubcALTVlem3  42106