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

Theorem neor 3033
Description: Logical OR with an equality. (Contributed by NM, 29-Apr-2007.)
Assertion
Ref Expression
neor ((𝐴 = 𝐵𝜓) ↔ (𝐴𝐵𝜓))

Proof of Theorem neor
StepHypRef Expression
1 df-or 848 . 2 ((𝐴 = 𝐵𝜓) ↔ (¬ 𝐴 = 𝐵𝜓))
2 df-ne 2940 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
32imbi1i 349 . 2 ((𝐴𝐵𝜓) ↔ (¬ 𝐴 = 𝐵𝜓))
41, 3bitr4i 278 1 ((𝐴 = 𝐵𝜓) ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wo 847   = wceq 1539  wne 2939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 207  df-or 848  df-ne 2940
This theorem is referenced by:  frsn  5772  ord0eln0  6438  fimaxre  12213  fiminre  12216  prime  12701  h1datomi  31601  elat2  32360  bnj563  34758  divrngidl  38036  dmncan1  38084  lkrshp4  39110  cvrcmp  39285  leat2  39296  isat3  39309  2llnmat  39527  2lnat  39787
  Copyright terms: Public domain W3C validator