Theorem sslin 3839

Description: Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.)

Assertion

Ref	Expression
sslin	|- ( A C_ B -> ( C i^i A ) C_ ( C i^i B ) )

Proof of Theorem sslin

Step	Hyp	Ref	Expression
1		ssrin 3838	. 2 |- ( A C_ B -> ( A i^i C ) C_ ( B i^i C ) )
2		incom 3805	. 2 |- ( C i^i A ) = ( A i^i C )
3		incom 3805	. 2 |- ( C i^i B ) = ( B i^i C )
4	1, 2, 3	3sstr4g 3646	1 |- ( A C_ B -> ( C i^i A ) C_ ( C i^i B ) )

Syntax hints:   -> wi 4   i^i cin 3573   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  ss2in  3840  ssres2  5425  ssrnres  5572  sbthlem7  8076  kmlem5  8976  canthnum  9471  ioodisj  12302  hashun3  13173  xpsc0  16220  dprdres  18427  dprd2da  18441  dmdprdsplit2lem  18444  cnprest  21093  isnrm3  21163  regsep2  21180  llycmpkgen2  21353  kqdisj  21535  regr1lem  21542  fclsbas  21825  fclscf  21829  flimfnfcls  21832  isfcf  21838  metdstri  22654  nulmbl2  23304  uniioombllem4  23354  volsup2  23373  volcn  23374  itg1climres  23481  limcresi  23649  limciun  23658  rlimcnp2  24693  rplogsum  25216  chssoc  28355  cmbr4i  28460  5oai  28520  3oalem6  28526  mdslmd4i  29192  atcvat4i  29256  imadifxp  29414  crefss  29916  pnfneige0  29997  cldbnd  32321  neibastop1  32354  neibastop2  32356  onint1  32448  oninhaus  32449  cntotbnd  33595  inxpssres  34076  polcon3N  35203  osumcllem4N  35245  lcfrlem2  36832  mapfzcons1  37280  coeq0i  37316  eldioph4b  37375  icccncfext  40100  srhmsubc  42076  fldc  42083  fldhmsubc  42084  rhmsubclem3  42088  srhmsubcALTV  42094  fldcALTV  42101  fldhmsubcALTV  42102  rhmsubcALTVlem4  42107