Theorem ssind 4172

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 512	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶))
4		ssin 4170	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶))
5	3, 4	sylib 217	1 ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 396   ∩ cin 3891   ⊆ wss 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909

This theorem is referenced by:  frrlem12  8104  frrlem13  8105  mreexexlem3d  17353  isacs1i  17364  rescabs  17545  rescabsOLD  17546  funcres2c  17615  lsmmod  19279  gsumzres  19508  gsumzsubmcl  19517  gsum2d  19571  issubdrg  20047  lspdisj  20385  mplind  21276  ntrin  22210  elcls  22222  neitr  22329  restcls  22330  lmss  22447  xkoinjcn  22836  trfg  23040  trust  23379  utoptop  23384  restutop  23387  isngp2  23751  lebnumii  24127  causs  24460  dvreslem  25071  c1lip3  25161  ssjo  29805  dmdbr5  30666  mdslj2i  30678  mdsl2bi  30681  mdslmd1lem2  30684  mdsymlem5  30765  difininv  30860  idlsrgmulrssin  31654  bnj1286  32995  mclsind  33528  neiin  34517  topmeet  34549  fnemeet2  34552  bj-elpwg  35221  bj-restpw  35259  bj-restb  35261  bj-restuni2  35265  idresssidinxp  36440  pmod1i  37858  dihmeetlem1N  39300  dihglblem5apreN  39301  dochdmj1  39400  mapdin  39672  baerlem3lem2  39720  baerlem5alem2  39721  baerlem5blem2  39722  trrelind  41243  isotone2  41629  nzin  41906  inmap  42719  islptre  43131  limccog  43132  limcresiooub  43154  limcresioolb  43155  limsupresxr  43278  liminfresxr  43279  liminfvalxr  43295  fourierdlem48  43666  fourierdlem49  43667  fourierdlem113  43731  pimiooltgt  44216  pimdecfgtioc  44220  pimincfltioc  44221  pimdecfgtioo  44222  pimincfltioo  44223  sssmf  44242  smflimlem2  44275  smfsuplem1  44312  iscnrm3llem2  46213  setrec2fun  46367