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

Metamath Proof Explorer

Theorem eqsstrdi

Description: A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017)

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

Proof

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