Metamath Proof Explorer


Theorem ssinss1

Description: Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999)

Ref Expression
Assertion ssinss1 ( 𝐴𝐶 → ( 𝐴𝐵 ) ⊆ 𝐶 )

Proof

Step Hyp Ref Expression
1 inss1 ( 𝐴𝐵 ) ⊆ 𝐴
2 sstr2 ( ( 𝐴𝐵 ) ⊆ 𝐴 → ( 𝐴𝐶 → ( 𝐴𝐵 ) ⊆ 𝐶 ) )
3 1 2 ax-mp ( 𝐴𝐶 → ( 𝐴𝐵 ) ⊆ 𝐶 )