MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ss2in Structured version   Visualization version   GIF version

Theorem ss2in 4201
Description: Intersection of subclasses. (Contributed by NM, 5-May-2000.)
Assertion
Ref Expression
ss2in ((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ⊆ (𝐵𝐷))

Proof of Theorem ss2in
StepHypRef Expression
1 ssrin 4198 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 sslin 4199 . 2 (𝐶𝐷 → (𝐵𝐶) ⊆ (𝐵𝐷))
31, 2sylan9ss 3960 1 ((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ⊆ (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  cin 3912  wss 3913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-in 3920  df-ss 3930
This theorem is referenced by:  disjxiun  5107  f1un  6809  undomOLD  9011  strleun  17040  dprdss  19822  dprd2da  19835  ablfac1b  19863  tgcl  22356  innei  22513  hausnei2  22741  bwth  22798  fbssfi  23225  fbunfip  23257  fgcl  23266  blin2  23819  vtxdun  28492  vtxdginducedm1  28554  5oai  30666  mayetes3i  30734  mdsl0  31315  neibastop1  34907  ismblfin  36192  heibor1lem  36341  pl42lem2N  38516  pl42lem3N  38517  ntrk2imkb  42431  ssin0  43385  iscnrm3llem2  47103
  Copyright terms: Public domain W3C validator