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

Metamath Proof Explorer

Theorem opeq12d

Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Hypotheses opeq1d.1 ⊢ φ → A = B
opeq12d.2 ⊢ φ → C = D
Assertion opeq12d ⊢ φ → A C = B D

Proof

Step Hyp Ref Expression
1 opeq1d.1 ⊢ φ → A = B
2 opeq12d.2 ⊢ φ → C = D
3 opeq12 ⊢ A = B ∧ C = D → A C = B D
4 1 2 3 syl2anc ⊢ φ → A C = B D