Theorem ss2in 3724

Description: Intersection of subclasses. (Contributed by NM, 5-May-2000.)

Assertion

Ref	Expression
ss2in

Proof of Theorem ss2in

Step	Hyp	Ref	Expression
1		ssrin 3722	. 2
2		sslin 3723	. 2
3	1, 2	sylan9ss 3516	1

Syntax hints:  ->wi 4  /\wa 369  i^icin 3474  C_wss 3475

This theorem is referenced by:  disjxiun  4449  undom  7625  strlemor1  14724  strleun  14727  dprdss  17076  dprd2da  17091  ablfac1b  17121  tgcl  19471  innei  19626  hausnei2  19854  bwth  19910  fbssfi  20338  fbunfip  20370  fgcl  20379  blin2  20932  vdgrun  24901  vdgrfiun  24902  5oai  26579  mayetes3i  26648  mdsl0  27229  ismblfin  30055  neibastop1  30177  heibor1lem  30305  pl42lem2N  35704  pl42lem3N  35705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489