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

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

Proof of Theorem ss2in
StepHypRef Expression
1 ssrin 4148 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 sslin 4149 . 2 (𝐶𝐷 → (𝐵𝐶) ⊆ (𝐵𝐷))
31, 2sylan9ss 3914 1 ((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ⊆ (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  cin 3865  wss 3866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-in 3873  df-ss 3883
This theorem is referenced by:  disjxiun  5050  undom  8733  strleun  16710  dprdss  19416  dprd2da  19429  ablfac1b  19457  tgcl  21866  innei  22022  hausnei2  22250  bwth  22307  fbssfi  22734  fbunfip  22766  fgcl  22775  blin2  23327  vtxdun  27569  vtxdginducedm1  27631  5oai  29742  mayetes3i  29810  mdsl0  30391  neibastop1  34285  ismblfin  35555  heibor1lem  35704  pl42lem2N  37731  pl42lem3N  37732  ntrk2imkb  41324  ssin0  42276  iscnrm3llem2  45917
  Copyright terms: Public domain W3C validator