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

Theorem neor 2873
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 384 . 2 ((𝐴 = 𝐵𝜓) ↔ (¬ 𝐴 = 𝐵𝜓))
2 df-ne 2782 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
32imbi1i 338 . 2 ((𝐴𝐵𝜓) ↔ (¬ 𝐴 = 𝐵𝜓))
41, 3bitr4i 266 1 ((𝐴 = 𝐵𝜓) ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wo 382   = wceq 1475  wne 2780
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 196  df-or 384  df-ne 2782
This theorem is referenced by:  frsn  5102  ord0eln0  5682  fimaxre  10820  prime  11293  h1datomi  27618  elat2  28377  bnj563  29861  divrngidl  32791  dmncan1  32839  lkrshp4  33207  cvrcmp  33382  leat2  33393  isat3  33406  2llnmat  33622  2lnat  33882
  Copyright terms: Public domain W3C validator