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

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

Proof of Theorem ss2in
StepHypRef Expression
1 ssrin 4192 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 sslin 4193 . 2 (𝐶𝐷 → (𝐵𝐶) ⊆ (𝐵𝐷))
31, 2sylan9ss 3956 1 ((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ⊆ (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  cin 3908  wss 3909
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 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3407  df-v 3446  df-in 3916  df-ss 3926
This theorem is referenced by:  disjxiun  5101  f1un  6802  undomOLD  9001  strleun  17026  dprdss  19804  dprd2da  19817  ablfac1b  19845  tgcl  22315  innei  22472  hausnei2  22700  bwth  22757  fbssfi  23184  fbunfip  23216  fgcl  23225  blin2  23778  vtxdun  28327  vtxdginducedm1  28389  5oai  30501  mayetes3i  30569  mdsl0  31150  neibastop1  34820  ismblfin  36108  heibor1lem  36257  pl42lem2N  38432  pl42lem3N  38433  ntrk2imkb  42289  ssin0  43243  iscnrm3llem2  46953
  Copyright terms: Public domain W3C validator