Metamath Proof Explorer

Theorem opeq12i

Description: Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006) (Proof shortened by Eric Schmidt, 4-Apr-2007)

Ref Expression
Hypotheses opeq1i.1 
|- A = B
opeq12i.2 
|- C = D
Assertion opeq12i 
|- <. A , C >. = <. B , D >.

Proof

Step Hyp Ref Expression
1 opeq1i.1 
 |-  A = B
2 opeq12i.2 
 |-  C = D
3 opeq12 
 |-  ( ( A = B /\ C = D ) -> <. A , C >. = <. B , D >. )
4 1 2 3 mp2an 
 |-  <. A , C >. = <. B , D >.