Theorem opeq12i 3163

Description: Equality inference for ordered pairs. (The proof was shortened by Eric Schmidt, 4-Apr-2007.)

Hypotheses

Ref	Expression
opeq1i.1	|- A = B
opeq12i.2	|- C = D

Assertion

Ref	Expression
opeq12i	|- <.A, C>. = <.B, D>.

Proof of Theorem opeq12i

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

Syntax hints:   = wceq 1298  <.cop 3046

This theorem is referenced by:  elxp6 5041  mulidpq 6221  prlem934b 6290  axi2m1 6438  ruclem15 8793  nvop2 9559  nvvop 9560  phop 9818  hhsssh 10772  dedalg 15090  catded 15111  txcnoprab 15911  isringd 16097  isdivrng1 16109

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-un 2600  df-sn 3049  df-pr 3050  df-op 3053

Copyright terms: Public domain