Theorem ss2in 3691

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

Assertion

Ref	Expression
ss2in

Proof of Theorem ss2in

Step	Hyp	Ref	Expression
1		ssrin 3689	. 2
2		sslin 3690	. 2
3	1, 2	sylan9ss 3483	1

Syntax hints:  ->wi 4  /\wa 369  i^icin 3441  C_wss 3442

This theorem is referenced by:  disjxiun  4406  undom  7533  strlemor1  14424  strleun  14427  dprdss  16701  dprd2da  16716  ablfac1b  16746  tgcl  18973  innei  19128  hausnei2  19356  bwth  19412  fbssfi  19809  fbunfip  19841  fgcl  19850  blin2  20403  vdgrun  24040  vdgrfiun  24041  5oai  25533  mayetes3i  25602  mdsl0  26183  ismblfin  28892  neibastop1  29040  heibor1lem  29168  icccncfext  30455  pl42lem2N  34475  pl42lem3N  34476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3083  df-in 3449  df-ss 3456