Theorem ssind 4231

Description: A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
ssind.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
ssind.2	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Assertion

Ref	Expression
ssind	⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∩ 𝐶))

Proof of Theorem ssind

Step	Hyp	Ref	Expression
1		ssind.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		ssind.2	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
3	1, 2	jca 510	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶))
4		ssin 4229	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶))
5	3, 4	sylib 217	1 ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 394   ∩ cin 3943   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-in 3951  df-ss 3961

This theorem is referenced by:  frrlem12  8303  frrlem13  8304  mreexexlem3d  17629  isacs1i  17640  rescabs  17821  rescabsOLD  17822  funcres2c  17893  lsmmod  19642  gsumzres  19876  gsumzsubmcl  19885  gsum2d  19939  issubdrg  20680  lspdisj  21025  mplind  22036  ntrin  23009  elcls  23021  neitr  23128  restcls  23129  lmss  23246  xkoinjcn  23635  trfg  23839  trust  24178  utoptop  24183  restutop  24186  isngp2  24550  lebnumii  24936  causs  25270  dvreslem  25882  c1lip3  25976  ssjo  31329  dmdbr5  32190  mdslj2i  32202  mdsl2bi  32205  mdslmd1lem2  32208  mdsymlem5  32289  difininv  32392  idlsrgmulrssin  33325  bnj1286  34781  mclsind  35311  neiin  35947  topmeet  35979  fnemeet2  35982  bj-elpwg  36662  bj-restpw  36702  bj-restb  36704  bj-restuni2  36708  idresssidinxp  37910  pmod1i  39451  dihmeetlem1N  40893  dihglblem5apreN  40894  dochdmj1  40993  mapdin  41265  baerlem3lem2  41313  baerlem5alem2  41314  baerlem5blem2  41315  trrelind  43237  isotone2  43621  nzin  43897  inmap  44721  islptre  45145  limccog  45146  limcresiooub  45168  limcresioolb  45169  limsupresxr  45292  liminfresxr  45293  liminfvalxr  45309  fourierdlem48  45680  fourierdlem49  45681  fourierdlem113  45745  pimiooltgt  46236  pimdecfgtioc  46241  pimincfltioc  46242  pimdecfgtioo  46243  pimincfltioo  46244  sssmf  46264  smflimlem2  46298  smfsuplem1  46337  iscnrm3llem2  48155  setrec2fun  48309