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

Theorem opeq12i 4806
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 4803 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
41, 2, 3mp2an 688 1 𝐴, 𝐶⟩ = ⟨𝐵, 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  cop 4569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570
This theorem is referenced by:  sbcop  5376  elxp6  7717  addcompq  10364  mulcompq  10366  addassnq  10372  mulassnq  10373  distrnq  10375  1lt2nq  10387  axi2m1  10573  om2uzrdg  13317  axlowdimlem6  26647  clwlkclwwlkflem  27696  konigsbergvtx  27939  konigsbergiedg  27940  nvop2  28299  nvvop  28300  phop  28509  hhsssh  28960  cshw1s2  30548  rngoi  35045  isdrngo1  35102
  Copyright terms: Public domain W3C validator