Metamath Proof Explorer


Theorem eqsstrdi

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

Ref Expression
Hypotheses eqsstrdi.1 φA=B
eqsstrdi.2 BC
Assertion eqsstrdi φAC

Proof

Step Hyp Ref Expression
1 eqsstrdi.1 φA=B
2 eqsstrdi.2 BC
3 2 a1i φBC
4 1 3 eqsstrd φAC