Metamath Proof Explorer


Theorem sseq12

Description: Equality theorem for the subclass relationship. (Contributed by NM, 31-May-1999)

Ref Expression
Assertion sseq12 A=BC=DACBD

Proof

Step Hyp Ref Expression
1 sseq1 A=BACBC
2 sseq2 C=DBCBD
3 1 2 sylan9bb A=BC=DACBD