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

Metamath Proof Explorer

Theorem sstri

Description: Subclass transitivity inference. (Contributed by NM, 5-May-2000)

Ref Expression
Hypotheses sstri.1 ⊢ A ⊆ B
sstri.2 ⊢ B ⊆ C
Assertion sstri ⊢ A ⊆ C

Proof

Step Hyp Ref Expression
1 sstri.1 ⊢ A ⊆ B
2 sstri.2 ⊢ B ⊆ C
3 sstr2 ⊢ A ⊆ B → B ⊆ C → A ⊆ C
4 1 2 3 mp2 ⊢ A ⊆ C