Theorem ss2in

Description: Intersection of subclasses. (Contributed by NM, 5-May-2000)

	Ref	Expression
Assertion	ss2in	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) → ( 𝐴 ∩ 𝐶 ) ⊆ ( 𝐵 ∩ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		ssrin	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∩ 𝐶 ) ⊆ ( 𝐵 ∩ 𝐶 ) )
2		sslin	⊢ ( 𝐶 ⊆ 𝐷 → ( 𝐵 ∩ 𝐶 ) ⊆ ( 𝐵 ∩ 𝐷 ) )
3	1 2	sylan9ss	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) → ( 𝐴 ∩ 𝐶 ) ⊆ ( 𝐵 ∩ 𝐷 ) )