This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) → ( 𝐴 ∩ 𝐶 ) ⊆ ( 𝐵 ∩ 𝐷 ) )