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

Theorem opeq12i 4763
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 4760 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
41, 2, 3mp2an 692 1 𝐴, 𝐶⟩ = ⟨𝐵, 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cop 4519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-un 3846  df-sn 4514  df-pr 4516  df-op 4520
This theorem is referenced by:  sbcop  5343  elxp6  7741  addcompq  10443  mulcompq  10445  addassnq  10451  mulassnq  10452  distrnq  10454  1lt2nq  10466  axi2m1  10652  om2uzrdg  13408  axlowdimlem6  26885  clwlkclwwlkflem  27933  konigsbergvtx  28175  konigsbergiedg  28176  nvop2  28535  nvvop  28536  phop  28745  hhsssh  29196  cshw1s2  30799  rngoi  35669  isdrngo1  35726
  Copyright terms: Public domain W3C validator