Metamath Proof Explorer


Theorem ss2in

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

Ref Expression
Assertion ss2in ⊢ A ⊆ B ∧ C ⊆ D → A ∩ C ⊆ B ∩ D

Proof

Step Hyp Ref Expression
1 ssrin ⊢ A ⊆ B → A ∩ C ⊆ B ∩ C
2 sslin ⊢ C ⊆ D → B ∩ C ⊆ B ∩ D
3 1 2 sylan9ss ⊢ A ⊆ B ∧ C ⊆ D → A ∩ C ⊆ B ∩ D