Theorem opeq12i 4845

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

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

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598

This theorem is used by:  sbcop  5473  elxp6  8026  addcompq  10952  mulcompq  10954  addassnq  10960  mulassnq  10961  distrnq  10963  1lt2nq  10975  axi2m1  11161  om2uzrdg  14012  pzriprng1ALT  21698  pzriprng1  21700  precsexlemcbv  28452  axlowdimlem6  29354  clwlkclwwlkflem  30424  konigsbergvtx  30670  konigsbergiedg  30671  nvop2  31033  nvvop  31034  phop  31243  hhsssh  31694  cshw1s2  33346  rngoi  38610  isdrngo1  38667  dfswapf2  50098  swapfcoa  50118  diag1a  50142  funcsetc1o  50334