Metamath Proof Explorer


Theorem sseqtrid

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

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

Proof

Step Hyp Ref Expression
1 sseqtrid.1 B A
2 sseqtrid.2 φ A = C
3 1 a1i φ B A
4 3 2 sseqtrd φ B C