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

Theorem opeq12i 4809
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 4806 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
41, 2, 3mp2an 689 1 𝐴, 𝐶⟩ = ⟨𝐵, 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539  cop 4567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568
This theorem is referenced by:  sbcop  5403  elxp6  7865  addcompq  10706  mulcompq  10708  addassnq  10714  mulassnq  10715  distrnq  10717  1lt2nq  10729  axi2m1  10915  om2uzrdg  13676  axlowdimlem6  27315  clwlkclwwlkflem  28368  konigsbergvtx  28610  konigsbergiedg  28611  nvop2  28970  nvvop  28971  phop  29180  hhsssh  29631  cshw1s2  31232  rngoi  36057  isdrngo1  36114
  Copyright terms: Public domain W3C validator