Theorem opeq1d 3825

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 3819	. 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 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:  oteq1  3828  oteq2  3829  opth  4281  cbvoprab2  6018  djuf1olem  7155  dfplpq2  7467  ltexnqq  7521  nnanq0  7571  addpinq1  7577  prarloclemlo  7607  prarloclem3  7610  prarloclem5  7613  prsrriota  7901  caucvgsrlemfv  7904  caucvgsr  7915  pitonnlem2  7960  pitonn  7961  recidpirq  7971  ax1rid  7990  axrnegex  7992  nntopi  8007  axcaucvglemval  8010  fseq1m1p1  10217  frecuzrdglem  10556  frecuzrdgg  10561  frecuzrdgdomlem  10562  frecuzrdgfunlem  10564  frecuzrdgsuctlem  10568  fsum2dlemstep  11745  fprod2dlemstep  11933  ennnfonelemp1  12777  ennnfonelemnn0  12793  setscomd  12873  imasaddvallemg  13147