Theorem opeq12d 2549

Description: Equality deduction for ordered pairs.

Hypotheses

Ref	Expression
opeq1d.1	|- (ph -> A = B)
opeq12d.2	|- (ph -> C = D)

Assertion

Ref	Expression
opeq12d	|- (ph -> <.A, C>. = <.B, D>.)

Proof of Theorem opeq12d

Step	Hyp	Ref	Expression
1		opeq1d.1	. . 3 |- (ph -> A = B)
2	1	opeq1d 2547	. 2 |- (ph -> <.A, C>. = <.B, C>.)
3		opeq12d.2	. . 3 |- (ph -> C = D)
4	3	opeq2d 2548	. 2 |- (ph -> <.B, C>. = <.B, D>.)
5	2, 4	eqtrd 1554	1 |- (ph -> <.A, C>. = <.B, D>.)

Syntax hints:   -> wi 3   = wceq 997  <.cop 2463

This theorem is referenced by:  xpassen 4504  xpdom2 4505  xpmapenlem4 4564  mapunen 4567  unidom 4870  addpipq 5119  mulsrpr 5250  mulcnsr 5319  mulresr 5322  ax1id 5347  axcnre 5351  seq1lem1 6568  seq1rval 6570  seq1suclem 6575  ruclem4 7605  xplmi 8058  xplm 8060  xpcn 8061  hhssnvt 9218  hhsssh 9222  11st22nd 10539  eloi 10741  homib 10806

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-v 1859  df-un 2101  df-sn 2464  df-pr 2465  df-op 2468

Copyright terms: Public domain