Theorem ssdif2d

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

	Ref	Expression
Hypotheses	ssdifd.1	|- ( ph -> A C_ B )
	ssdif2d.2	|- ( ph -> C C_ D )
Assertion	ssdif2d	|- ( ph -> ( A \ D ) C_ ( B \ C ) )

Proof

Step	Hyp	Ref	Expression
1		ssdifd.1	|- ( ph -> A C_ B )
2		ssdif2d.2	|- ( ph -> C C_ D )
3	2	sscond	|- ( ph -> ( A \ D ) C_ ( A \ C ) )
4	1	ssdifd	|- ( ph -> ( A \ C ) C_ ( B \ C ) )
5	3 4	sstrd	|- ( ph -> ( A \ D ) C_ ( B \ C ) )