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

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

Proof of Theorem ss2in
StepHypRef Expression
1 ssrin 4160 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 sslin 4161 . 2 (𝐶𝐷 → (𝐵𝐶) ⊆ (𝐵𝐷))
31, 2sylan9ss 3928 1 ((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ⊆ (𝐵𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∩ cin 3880   ⊆ wss 3881 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898 This theorem is referenced by:  disjxiun  5027  undom  8590  strleun  16585  dprdss  19147  dprd2da  19160  ablfac1b  19188  tgcl  21581  innei  21737  hausnei2  21965  bwth  22022  fbssfi  22449  fbunfip  22481  fgcl  22490  blin2  23043  vtxdun  27278  vtxdginducedm1  27340  5oai  29451  mayetes3i  29519  mdsl0  30100  neibastop1  33832  ismblfin  35114  heibor1lem  35263  pl42lem2N  37292  pl42lem3N  37293  ntrk2imkb  40755  ssin0  41704
 Copyright terms: Public domain W3C validator