Theorem ssdifd 3625

Description: If A is contained in B, then ( A \ C ) is contained in ( B \ C ). Deduction form of ssdif 3624. (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 3624	. 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 3458   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-dif 3464  df-in 3468  df-ss 3475

This theorem is referenced by:  ssdif2d  3628  domunsncan  7619  fin1a2lem13  8795  seqcoll2  12494  rpnnen2lem11  13939  mrieqv2d  15017  mrissmrid  15019  mreexexlem4d  15025  acsfiindd  15785  lsppratlem3  17773  lsppratlem4  17774  f1lindf  18834  lpss3  19622  lpcls  19842  fin1aufil  20410  rrxmval  21809  rrxmetlem  21811  uniioombllem3  21971  i1fmul  22080  itg1addlem4  22083  itg1climres  22098  limciun  22275  ig1peu  22549  ig1pdvds  22554  nbgrassovt  24411  usgreghash2spotv  25042  sitgclg  28261  mthmpps  28919  dochfln0  36944  lcfl6  36967  lcfrlem16  37025  hdmaprnlem4N  37323