Metamath Proof Explorer


Theorem ssinss1OLD

Description: Obsolete version of ssinss1 as of 10-Jun-2026. (Contributed by NM, 14-Sep-1999) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ssinss1OLD ⊢ A ⊆ C → A ∩ B ⊆ C

Proof

Step Hyp Ref Expression
1 inss1 ⊢ A ∩ B ⊆ A
2 sstr2 ⊢ A ∩ B ⊆ A → A ⊆ C → A ∩ B ⊆ C
3 1 2 ax-mp ⊢ A ⊆ C → A ∩ B ⊆ C