Theorem ssdifssd 3748

Description: If A is contained in B, then ( A \ C ) is also contained in B. Deduction form of ssdifss 3741. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
ssdifd.1	|- ( ph -> A C_ B )

Assertion

Ref	Expression
ssdifssd	|- ( ph -> ( A \ C ) C_ B )

Proof of Theorem ssdifssd

Step	Hyp	Ref	Expression
1		ssdifd.1	. 2 |- ( ph -> A C_ B )
2		ssdifss 3741	. 2 |- ( A C_ B -> ( A \ C ) C_ B )
3	1, 2	syl 17	1 |- ( ph -> ( A \ C ) C_ B )

Syntax hints:   -> wi 4   \ cdif 3571   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-dif 3577  df-in 3581  df-ss 3588

This theorem is referenced by:  unblem1  8212  fin23lem26  9147  fin23lem29  9163  isf32lem8  9182  fprodfvdvdsd  15058  mrieqvlemd  16289  mrieqv2d  16299  mrissmrid  16301  mreexmrid  16303  mreexexlem2d  16305  mreexexlem4d  16307  acsfiindd  17177  ablfac1eulem  18471  lbspss  19082  lspsolv  19143  lsppratlem3  19149  lsppratlem4  19150  lspprat  19153  islbs2  19154  islbs3  19155  lbsextlem2  19159  lbsextlem3  19160  lbsextlem4  19161  lpss3  20948  islp3  20950  neitr  20984  restlp  20987  lpcls  21168  qtoprest  21520  ufinffr  21733  cldsubg  21914  xrge0gsumle  22636  bcthlem5  23125  rrxmval  23188  cmmbl  23302  nulmbl2  23304  shftmbl  23306  iundisj2  23317  uniiccdif  23346  uniiccmbl  23358  itg1val2  23451  itg1cl  23452  itg1ge0  23453  i1fadd  23462  itg1addlem5  23467  i1fmulc  23470  itg1mulc  23471  itg10a  23477  itg1ge0a  23478  itg1climres  23481  mbfi1fseqlem4  23485  itgss3  23581  limcdif  23640  limcnlp  23642  limcmpt2  23648  perfdvf  23667  dvcnp2  23683  dvaddbr  23701  dvmulbr  23702  dvferm1  23748  dvferm2  23750  ftc1lem6  23804  ig1peu  23931  ig1pdvds  23936  taylthlem1  24127  taylthlem2  24128  ulmdvlem3  24156  rlimcnp  24692  wilthlem2  24795  elpwdifcl  29358  iundisj2f  29403  ofpreima2  29466  iundisj2fi  29556  omsmeas  30385  eulerpartlemgs2  30442  ballotlemfrc  30588  hgt750lemd  30726  hgt750leme  30736  cvmscld  31255  unbdqndv1  32499  lindsenlbs  33404  ftc1cnnc  33484  lsatfixedN  34296  dochsnkr  36761  hdmaprnlem4tN  37144  cntzsdrg  37772  supminfxr2  39699  limcrecl  39861  cnrefiisplem  40055  fperdvper  40133  ismbl3  40203  ovolsplit  40205  ismbl4  40210  stoweidlem57  40274  dirkercncflem3  40322  fourierdlem42  40366  fourierdlem46  40369  fourierdlem62  40385  caragenuncllem  40726  caragendifcl  40728  omelesplit  40732  carageniuncllem2  40736  carageniuncl  40737  caragenel2d  40746  hspmbllem3  40842  hspmbl  40843  ovnsplit  40862  vonvolmbllem  40874  vonvolmbl  40875  c0rnghm  41913  lincdifsn  42213  lindslinindsimp1  42246  lincresunit3lem2  42269