Theorem opeq12i 4848

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

This proof depends on syntax axioms:   = wceq 1569  ⟨cop 4838

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839

This theorem is used by:  sbcop  5463  elxp6  8045  addcompq  11048  mulcompq  11050  addassnq  11056  mulassnq  11057  distrnq  11059  1lt2nq  11071  axi2m1  11257  om2uzrdg  14112  pzriprng1ALT  21817  pzriprng1  21819  precsexlemcbv  28607  axlowdimlem6  29540  clwlkclwwlkflem  30610  konigsbergvtx  30862  konigsbergiedg  30863  nvop2  31225  nvvop  31226  phop  31435  hhsssh  31886  cshw1s2  33577  rngoi  38976  isdrngo1  39033  dfswapf2  50525  swapfcoa  50545  diag1a  50569  funcsetc1o  50774