Metamath Proof Explorer
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25Apr2004)


Ref 
Expression 

Hypotheses 
sseqtrrd.1 
 ( ph > A C_ B ) 


sseqtrrd.2 
 ( ph > C = B ) 

Assertion 
sseqtrrd 
 ( ph > A C_ C ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

sseqtrrd.1 
 ( ph > A C_ B ) 
2 

sseqtrrd.2 
 ( ph > C = B ) 
3 
2

eqcomd 
 ( ph > B = C ) 
4 
1 3

sseqtrd 
 ( ph > A C_ C ) 