Theorem opeq2d 3826

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

Hypothesis

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

Assertion

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

Proof of Theorem opeq2d

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

Syntax hints:   -> wi 4   = wceq 1373   <.cop 3636

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642

This theorem is referenced by:  tfr1onlemaccex  6436  tfrcllemaccex  6449  fundmen  6900  exmidapne  7374  recexnq  7505  suplocexprlemex  7837  elreal2  7945  frecuzrdgrrn  10555  frec2uzrdg  10556  frecuzrdgrcl  10557  frecuzrdgsuc  10561  frecuzrdgrclt  10562  frecuzrdgg  10563  frecuzrdgsuctlem  10570  seqeq2  10598  seqeq3  10599  iseqvalcbv  10606  seq3val  10607  seqvalcd  10608  s1val  11074  s1eq  11076  s1prc  11080  swrdlsw  11125  eucalgval  12409  ennnfonelemp1  12810  ennnfonelemnn0  12826  strsetsid  12898  ressvalsets  12929  strressid  12936  ressinbasd  12939  ressressg  12940  prdsex  13134  prdsval  13138  imasex  13170  imasival  13171  imasaddvallemg  13180  xpsfval  13213  xpsval  13217  mgpvalg  13718  mgpress  13726  ring1  13854  opprvalg  13864  sraval  14232  zlmval  14422  znval  14431  znval2  14433  psrval  14461