Theorem ssdifd 3513

Description: If A is contained in B, then ( A \ C ) is contained in ( B \ C ). Deduction form of ssdif 3512. (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 3512	. 2 |- ( A C_ B -> ( A \ C ) C_ ( B \ C ) )
3	1, 2	syl 16	1 |- ( ph -> ( A \ C ) C_ ( B \ C ) )

Syntax hints:   -> wi 4   \ cdif 3346   C_ wss 3349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-dif 3352  df-in 3356  df-ss 3363

This theorem is referenced by:  ssdif2d  3516  domunsncan  7432  fin1a2lem13  8602  seqcoll2  12238  rpnnen2lem11  13528  mrieqv2d  14598  mrissmrid  14600  mreexexlem4d  14606  acsfiindd  15368  lsppratlem3  17252  lsppratlem4  17253  f1lindf  18273  lpss3  18770  lpcls  18990  fin1aufil  19527  rrxmval  20926  rrxmetlem  20928  uniioombllem3  21087  i1fmul  21196  itg1addlem4  21199  itg1climres  21214  limciun  21391  ig1peu  21665  ig1pdvds  21670  nbgrassovt  23368  sitgclg  26750  usgreghash2spotv  30685  dochfln0  35218  lcfl6  35241  lcfrlem16  35299  hdmaprnlem4N  35597