Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  opeq12i Structured version   Visualization version   GIF version

Theorem opeq12i 4345
 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
StepHypRef Expression
1 opeq1i.1 . 2 𝐴 = 𝐵
2 opeq12i.2 . 2 𝐶 = 𝐷
3 opeq12 4342 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
41, 2, 3mp2an 704 1 𝐴, 𝐶⟩ = ⟨𝐵, 𝐷
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475  ⟨cop 4131 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132 This theorem is referenced by:  elxp6  7091  addcompq  9651  mulcompq  9653  addassnq  9659  mulassnq  9660  distrnq  9662  1lt2nq  9674  axi2m1  9859  om2uzrdg  12617  axlowdimlem6  25627  nvop2  26847  nvvop  26848  phop  27057  hhsssh  27510  rngoi  32868  isdrngo1  32925  konigsbergvtx  41414  konigsbergiedg  41415
 Copyright terms: Public domain W3C validator