Theorem opeq1d 3828

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 3822	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
3	1, 2	syl 14	1 ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   = wceq 1373  ⟨cop 3638

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 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3172  df-sn 3641  df-pr 3642  df-op 3644

This theorem is referenced by:  oteq1  3831  oteq2  3832  opth  4286  cbvoprab2  6028  djuf1olem  7167  dfplpq2  7480  ltexnqq  7534  nnanq0  7584  addpinq1  7590  prarloclemlo  7620  prarloclem3  7623  prarloclem5  7626  prsrriota  7914  caucvgsrlemfv  7917  caucvgsr  7928  pitonnlem2  7973  pitonn  7974  recidpirq  7984  ax1rid  8003  axrnegex  8005  nntopi  8020  axcaucvglemval  8023  fseq1m1p1  10230  frecuzrdglem  10569  frecuzrdgg  10574  frecuzrdgdomlem  10575  frecuzrdgfunlem  10577  frecuzrdgsuctlem  10581  pfxswrd  11171  fsum2dlemstep  11795  fprod2dlemstep  11983  ennnfonelemp1  12827  ennnfonelemnn0  12843  setscomd  12923  imasaddvallemg  13197