Theorem opeq1d 3810

Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)

Hypothesis

Ref	Expression
opeq1d.1	|- ( ph -> A = B )

Assertion

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

Proof of Theorem opeq1d

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 |- ( ph -> A = B )
2		opeq1 3804	. 2 |- ( A = B -> <. A , C >. = <. B , C >. )
3	1, 2	syl 14	1 |- ( ph -> <. A , C >. = <. B , C >. )

Syntax hints:   -> wi 4   = wceq 1364   <.cop 3621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627

This theorem is referenced by:  oteq1  3813  oteq2  3814  opth  4266  cbvoprab2  5991  djuf1olem  7112  dfplpq2  7414  ltexnqq  7468  nnanq0  7518  addpinq1  7524  prarloclemlo  7554  prarloclem3  7557  prarloclem5  7560  prsrriota  7848  caucvgsrlemfv  7851  caucvgsr  7862  pitonnlem2  7907  pitonn  7908  recidpirq  7918  ax1rid  7937  axrnegex  7939  nntopi  7954  axcaucvglemval  7957  fseq1m1p1  10161  frecuzrdglem  10482  frecuzrdgg  10487  frecuzrdgdomlem  10488  frecuzrdgfunlem  10490  frecuzrdgsuctlem  10494  fsum2dlemstep  11577  fprod2dlemstep  11765  ennnfonelemp1  12563  ennnfonelemnn0  12579  setscomd  12659  imasaddvallemg  12898