Metamath Proof Explorer


Theorem eqsstrrdi

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

Ref Expression
Hypotheses eqsstrrdi.1 φ B = A
eqsstrrdi.2 B C
Assertion eqsstrrdi φ A C

Proof

Step Hyp Ref Expression
1 eqsstrrdi.1 φ B = A
2 eqsstrrdi.2 B C
3 1 eqcomd φ A = B
4 3 2 eqsstrdi φ A C