Metamath Proof Explorer


Theorem sstri

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

Ref Expression
Hypotheses sstri.1 𝐴𝐵
sstri.2 𝐵𝐶
Assertion sstri 𝐴𝐶

Proof

Step Hyp Ref Expression
1 sstri.1 𝐴𝐵
2 sstri.2 𝐵𝐶
3 sstr2 ( 𝐴𝐵 → ( 𝐵𝐶𝐴𝐶 ) )
4 1 2 3 mp2 𝐴𝐶