Theorem ssind 3980

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

Syntax hints:   → wi 4   ∧ wa 383   ∩ cin 3714   ⊆ wss 3715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722  df-ss 3729

This theorem is referenced by:  mreexexlem3d  16508  isacs1i  16519  rescabs  16694  funcres2c  16762  lsmmod  18288  gsumzres  18510  gsumzsubmcl  18518  gsum2d  18571  issubdrg  19007  lspdisj  19327  mplind  19704  ntrin  21067  elcls  21079  neitr  21186  restcls  21187  lmss  21304  xkoinjcn  21692  trfg  21896  trust  22234  utoptop  22239  restutop  22242  isngp2  22602  lebnumii  22966  causs  23296  dvreslem  23872  c1lip3  23961  ssjo  28615  dmdbr5  29476  mdslj2i  29488  mdsl2bi  29491  mdslmd1lem2  29494  mdsymlem5  29575  difininv  29661  bnj1286  31394  mclsind  31774  neiin  32633  topmeet  32665  fnemeet2  32668  bj-restpw  33351  bj-restb  33353  bj-restuni2  33357  idresssidinxp  34403  pmod1i  35637  dihmeetlem1N  37081  dihglblem5apreN  37082  dochdmj1  37181  mapdin  37453  baerlem3lem2  37501  baerlem5alem2  37502  baerlem5blem2  37503  trrelind  38459  isotone2  38849  nzin  39019  inmap  39900  islptre  40354  limccog  40355  limcresiooub  40377  limcresioolb  40378  limsupresxr  40501  liminfresxr  40502  liminfvalxr  40518  fourierdlem48  40874  fourierdlem49  40875  fourierdlem113  40939  pimiooltgt  41427  pimdecfgtioc  41431  pimincfltioc  41432  pimdecfgtioo  41433  pimincfltioo  41434  sssmf  41453  smflimlem2  41486  smfsuplem1  41523  setrec2fun  42949