Metamath Proof Explorer

Theorem 3sstr4g

Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 16-Aug-1994) (Proof shortened by Eric Schmidt, 26-Jan-2007)

Ref Expression
Hypotheses 3sstr4g.1 φ A B
3sstr4g.2 C = A
3sstr4g.3 D = B
Assertion 3sstr4g φ C D


Step Hyp Ref Expression
1 3sstr4g.1 φ A B
2 3sstr4g.2 C = A
3 3sstr4g.3 D = B
4 2 3 sseq12i C D A B
5 1 4 sylibr φ C D