Metamath Proof Explorer


Theorem sseqtrdi

Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004)

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

Proof

Step Hyp Ref Expression
1 sseqtrdi.1 φ A B
2 sseqtrdi.2 B = C
3 2 sseq2i A B A C
4 1 3 sylib φ A C