Metamath Proof Explorer


Theorem sstrid

Description: Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014)

Ref Expression
Hypotheses sstrid.1 𝐴𝐵
sstrid.2 ( 𝜑𝐵𝐶 )
Assertion sstrid ( 𝜑𝐴𝐶 )

Proof

Step Hyp Ref Expression
1 sstrid.1 𝐴𝐵
2 sstrid.2 ( 𝜑𝐵𝐶 )
3 1 a1i ( 𝜑𝐴𝐵 )
4 3 2 sstrd ( 𝜑𝐴𝐶 )