Theorem opeq12i 4837

Description: Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)

Hypotheses

Ref	Expression
opeq1i.1	⊢ 𝐴 = 𝐵
opeq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
opeq12i	⊢ ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩

Proof of Theorem opeq12i

Step	Hyp	Ref	Expression
1		opeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		opeq12i.2	. 2 ⊢ 𝐶 = 𝐷
3		opeq12 4834	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
4	1, 2, 3	mp2an 702	1 ⊢ ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩

Syntax hints:   = wceq 1561  ⟨cop 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590

This theorem is referenced by:  sbcop  5458  elxp6  8005  addcompq  10909  mulcompq  10911  addassnq  10917  mulassnq  10918  distrnq  10920  1lt2nq  10932  axi2m1  11118  om2uzrdg  13970  pzriprng1ALT  21549  pzriprng1  21551  precsexlemcbv  28300  axlowdimlem6  29149  clwlkclwwlkflem  30207  konigsbergvtx  30449  konigsbergiedg  30450  nvop2  30812  nvvop  30813  phop  31022  hhsssh  31473  cshw1s2  33139  rngoi  38399  isdrngo1  38456  dfswapf2  49883  swapfcoa  49903  diag1a  49927  funcsetc1o  50119