Theorem opeq12d 2500

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

Syntax hints:   -> wi 3   = wceq 958  <.cop 2416

This theorem is referenced by:  xpassen 4448  xpdom2 4449  xpmapenlem4 4506  mapunen 4509  unidom 4825  addpipq 5073  mulsrpr 5204  mulcnsr 5273  mulresr 5276  ax1id 5301  axcnre 5305  seq1lem1 6317  seq1rval 6319  seq1suclem 6324  ruclem4 7521  xplmi 7977  xplm 7979  xpcn 7980  hhssnvt 9137  hhsssh 9141  11st22nd 10456  eloi 10638  homib 10703

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-un 2054  df-sn 2417  df-pr 2418  df-op 2421

Copyright terms: Public domain