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

Metamath Proof Explorer

Theorem sseqtrrid

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

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

Proof

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