This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 = 𝐵
psseq12i.2 ⊢ 𝐶 = 𝐷
Assertion psseq12i ( 𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐷 )

Proof

Step Hyp Ref Expression
1 psseq1i.1 ⊢ 𝐴 = 𝐵
2 psseq12i.2 ⊢ 𝐶 = 𝐷
3 1 psseq1i ⊢ ( 𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶 )
4 2 psseq2i ⊢ ( 𝐵 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐷 )
5 3 4 bitri ⊢ ( 𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐷 )