Metamath Proof Explorer


Theorem sseqtrid

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

Ref Expression
Hypotheses sseqtrid.1
|- B C_ A
sseqtrid.2
|- ( ph -> A = C )
Assertion sseqtrid
|- ( ph -> B C_ C )

Proof

Step Hyp Ref Expression
1 sseqtrid.1
 |-  B C_ A
2 sseqtrid.2
 |-  ( ph -> A = C )
3 1 a1i
 |-  ( ph -> B C_ A )
4 3 2 sseqtrd
 |-  ( ph -> B C_ C )