Theorem ssdifd 3580

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

Hypothesis

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

Assertion

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

Proof of Theorem ssdifd

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

Syntax hints:   -> wi 4   \ cdif 3412   C_ wss 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-dif 3418  df-in 3422  df-ss 3429

This theorem is referenced by:  ssdif2d  3583  domunsncan  7697  fin1a2lem13  8867  seqcoll2  12660  rpnnen2lem11  14325  coprmprod  14726  mrieqv2d  15593  mrissmrid  15595  mreexexlem4d  15601  acsfiindd  16471  lsppratlem3  18420  lsppratlem4  18421  f1lindf  19428  lpss3  20208  lpcls  20428  fin1aufil  20995  rrxmval  22407  rrxmetlem  22409  uniioombllem3  22591  i1fmul  22702  itg1addlem4  22705  itg1climres  22720  limciun  22897  ig1peu  23170  ig1peuOLD  23171  ig1pdvds  23176  ig1pdvdsOLD  23182  nbgrassovt  25211  usgreghash2spotv  25842  sitgclg  29223  mthmpps  30268  poimirlem11  31995  poimirlem12  31996  poimirlem15  31999  dochfln0  35089  lcfl6  35112  lcfrlem16  35170  hdmaprnlem4N  35468  caragendifcl  38372