Theorem opeq12d 2491

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 2489	. 2 |- (ph -> <.A, C>. = <.B, C>.)
3		opeq12d.2	. . 3 |- (ph -> C = D)
4	3	opeq2d 2490	. 2 |- (ph -> <.B, C>. = <.B, D>.)
5	2, 4	eqtrd 1504	1 |- (ph -> <.A, C>. = <.B, D>.)

Syntax hints:   -> wi 3   = wceq 954  <.cop 2407

This theorem is referenced by:  xpassen 4427  xpdom2 4428  xpmapenlem4 4485  mapunen 4488  unidom 4788  addpipq 5034  mulsrpr 5165  mulcnsr 5234  mulresr 5237  ax1id 5262  axcnre 5266  seq1lem1 6254  seq1rval 6256  seq1suclem 6261  ruclem4 7464  xplmi 7923  xplm 7925  xpcn 7926  hhssnvt 9074  hhsssh 9078  11st22nd 10390  eloi 10539  homib 10604

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-un 2046  df-sn 2408  df-pr 2409  df-op 2412

Copyright terms: Public domain