Metamath Proof Explorer


Theorem sseqtrid

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

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

Proof

Step Hyp Ref Expression
1 sseqtrid.1 𝐵𝐴
2 sseqtrid.2 ( 𝜑𝐴 = 𝐶 )
3 1 a1i ( 𝜑𝐵𝐴 )
4 3 2 sseqtrd ( 𝜑𝐵𝐶 )