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  6434  tfrcllemaccex  6447  fundmen  6898  exmidapne  7372  recexnq  7503  suplocexprlemex  7835  elreal2  7943  frecuzrdgrrn  10553  frec2uzrdg  10554  frecuzrdgrcl  10555  frecuzrdgsuc  10559  frecuzrdgrclt  10560  frecuzrdgg  10561  frecuzrdgsuctlem  10568  seqeq2  10596  seqeq3  10597  iseqvalcbv  10604  seq3val  10605  seqvalcd  10606  s1val  11071  s1eq  11073  s1prc  11077  swrdlsw  11122  eucalgval  12376  ennnfonelemp1  12777  ennnfonelemnn0  12793  strsetsid  12865  ressvalsets  12896  strressid  12903  ressinbasd  12906  ressressg  12907  prdsex  13101  prdsval  13105  imasex  13137  imasival  13138  imasaddvallemg  13147  xpsfval  13180  xpsval  13184  mgpvalg  13685  mgpress  13693  ring1  13821  opprvalg  13831  sraval  14199  zlmval  14389  znval  14398  znval2  14400  psrval  14428