Metamath Proof Explorer


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 ( 𝜑𝐴𝐵 )
ssdif2d.2 ( 𝜑𝐶𝐷 )
Assertion ssdif2d ( 𝜑 → ( 𝐴𝐷 ) ⊆ ( 𝐵𝐶 ) )

Proof

Step Hyp Ref Expression
1 ssdifd.1 ( 𝜑𝐴𝐵 )
2 ssdif2d.2 ( 𝜑𝐶𝐷 )
3 2 sscond ( 𝜑 → ( 𝐴𝐷 ) ⊆ ( 𝐴𝐶 ) )
4 1 ssdifd ( 𝜑 → ( 𝐴𝐶 ) ⊆ ( 𝐵𝐶 ) )
5 3 4 sstrd ( 𝜑 → ( 𝐴𝐷 ) ⊆ ( 𝐵𝐶 ) )