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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  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  5459  elxp6  8035  addcompq  11035  mulcompq  11037  addassnq  11043  mulassnq  11044  distrnq  11046  1lt2nq  11058  axi2m1  11244  om2uzrdg  14099  pzriprng1ALT  21802  pzriprng1  21804  precsexlemcbv  28592  axlowdimlem6  29525  clwlkclwwlkflem  30595  konigsbergvtx  30847  konigsbergiedg  30848  nvop2  31210  nvvop  31211  phop  31420  hhsssh  31871  cshw1s2  33521  rngoi  38833  isdrngo1  38890  dfswapf2  50368  swapfcoa  50388  diag1a  50412  funcsetc1o  50604