Theorem opeq1d 3839

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 3833	. 2 |- ( A = B -> <. A , C >. = <. B , C >. )
3	1, 2	syl 14	1 |- ( ph -> <. A , C >. = <. B , C >. )

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

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652

This theorem is referenced by:  oteq1  3842  oteq2  3843  opth  4299  cbvoprab2  6041  djuf1olem  7181  dfplpq2  7502  ltexnqq  7556  nnanq0  7606  addpinq1  7612  prarloclemlo  7642  prarloclem3  7645  prarloclem5  7648  prsrriota  7936  caucvgsrlemfv  7939  caucvgsr  7950  pitonnlem2  7995  pitonn  7996  recidpirq  8006  ax1rid  8025  axrnegex  8027  nntopi  8042  axcaucvglemval  8045  fseq1m1p1  10252  frecuzrdglem  10593  frecuzrdgg  10598  frecuzrdgdomlem  10599  frecuzrdgfunlem  10601  frecuzrdgsuctlem  10605  pfxswrd  11197  swrdccat  11226  swrdccat3blem  11230  fsum2dlemstep  11860  fprod2dlemstep  12048  ennnfonelemp1  12892  ennnfonelemnn0  12908  setscomd  12988  imasaddvallemg  13262