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

Metamath Proof Explorer

Theorem preq12d

Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012)

Ref Expression
Hypotheses preq1d.1 ⊢ φ → A = B
preq12d.2 ⊢ φ → C = D
Assertion preq12d ⊢ φ → A C = B D

Proof

Step Hyp Ref Expression
1 preq1d.1 ⊢ φ → A = B
2 preq12d.2 ⊢ φ → C = D
3 preq12 ⊢ A = B ∧ C = D → A C = B D
4 1 2 3 syl2anc ⊢ φ → A C = B D