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

Metamath Proof Explorer

Theorem preq2

Description: Equality theorem for unordered pairs. (Contributed by NM, 15-Jul-1993)

Ref Expression
Assertion preq2 ⊢ A = B → C A = C B

Proof

Step Hyp Ref Expression
1 preq1 ⊢ A = B → A C = B C
2 prcom ⊢ C A = A C
3 prcom ⊢ C B = B C
4 1 2 3 3eqtr4g ⊢ A = B → C A = C B