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

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

Proof of Theorem ss2in
StepHypRef Expression
1 ssrin 3818 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 sslin 3819 . 2 (𝐶𝐷 → (𝐵𝐶) ⊆ (𝐵𝐷))
31, 2sylan9ss 3597 1 ((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ⊆ (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  cin 3555  wss 3556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-in 3563  df-ss 3570
This theorem is referenced by:  disjxiun  4611  disjxiunOLD  4612  undom  7995  strlemor1OLD  15893  strleun  15896  dprdss  18352  dprd2da  18365  ablfac1b  18393  tgcl  20687  innei  20842  hausnei2  21070  bwth  21126  fbssfi  21554  fbunfip  21586  fgcl  21595  blin2  22147  vtxdun  26270  5oai  28381  mayetes3i  28449  mdsl0  29030  neibastop1  32017  ismblfin  33103  heibor1lem  33261  pl42lem2N  34767  pl42lem3N  34768  ntrk2imkb  37838  ssin0  38727
  Copyright terms: Public domain W3C validator