Metamath Proof Explorer

Theorem 3sstr4d

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

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


Step Hyp Ref Expression
1 3sstr4d.1 φ A B
2 3sstr4d.2 φ C = A
3 3sstr4d.3 φ D = B
4 2 3 sseq12d φ C D A B
5 1 4 mpbird φ C D