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

Theorem opeq12i 4800
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 4797 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
41, 2, 3mp2an 688 1 𝐴, 𝐶⟩ = ⟨𝐵, 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  cop 4563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564
This theorem is referenced by:  sbcop  5371  elxp6  7712  addcompq  10360  mulcompq  10362  addassnq  10368  mulassnq  10369  distrnq  10371  1lt2nq  10383  axi2m1  10569  om2uzrdg  13312  axlowdimlem6  26660  clwlkclwwlkflem  27709  konigsbergvtx  27952  konigsbergiedg  27953  nvop2  28312  nvvop  28313  phop  28522  hhsssh  28973  cshw1s2  30561  rngoi  35058  isdrngo1  35115
  Copyright terms: Public domain W3C validator