Theorem opeq1d 3814

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

Hypothesis

Ref	Expression
opeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
opeq1d	⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Proof of Theorem opeq1d

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		opeq1 3808	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
3	1, 2	syl 14	1 ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   = wceq 1364  ⟨cop 3625

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631

This theorem is referenced by:  oteq1  3817  oteq2  3818  opth  4270  cbvoprab2  5995  djuf1olem  7119  dfplpq2  7421  ltexnqq  7475  nnanq0  7525  addpinq1  7531  prarloclemlo  7561  prarloclem3  7564  prarloclem5  7567  prsrriota  7855  caucvgsrlemfv  7858  caucvgsr  7869  pitonnlem2  7914  pitonn  7915  recidpirq  7925  ax1rid  7944  axrnegex  7946  nntopi  7961  axcaucvglemval  7964  fseq1m1p1  10170  frecuzrdglem  10503  frecuzrdgg  10508  frecuzrdgdomlem  10509  frecuzrdgfunlem  10511  frecuzrdgsuctlem  10515  fsum2dlemstep  11599  fprod2dlemstep  11787  ennnfonelemp1  12623  ennnfonelemnn0  12639  setscomd  12719  imasaddvallemg  12958