Theorem opeq12i 4838

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 4835	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
4	1, 2, 3	mp2an 705	1 ⊢ ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩

This proof depends on syntax axioms:   = wceq 1570  ⟨cop 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591

This theorem is used by:  sbcop  5465  elxp6  8021  addcompq  10962  mulcompq  10964  addassnq  10970  mulassnq  10971  distrnq  10973  1lt2nq  10985  axi2m1  11171  om2uzrdg  14023  pzriprng1ALT  21712  pzriprng1  21714  precsexlemcbv  28474  axlowdimlem6  29407  clwlkclwwlkflem  30477  konigsbergvtx  30729  konigsbergiedg  30730  nvop2  31092  nvvop  31093  phop  31302  hhsssh  31753  cshw1s2  33403  rngoi  38652  isdrngo1  38709  dfswapf2  50190  swapfcoa  50210  diag1a  50234  funcsetc1o  50426