Metamath Proof Explorer


Theorem psseq12i

Description: An equality inference for the proper subclass relationship. (Contributed by NM, 9-Jun-2004)

Ref Expression
Hypotheses psseq1i.1 A=B
psseq12i.2 C=D
Assertion psseq12i ACBD

Proof

Step Hyp Ref Expression
1 psseq1i.1 A=B
2 psseq12i.2 C=D
3 1 psseq1i ACBC
4 2 psseq2i BCBD
5 3 4 bitri ACBD