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 A C B D

Proof

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