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

Theorem neor 3023
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 2933 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
32imbi1i 338 . 2 ((𝐴𝐵𝜓) ↔ (¬ 𝐴 = 𝐵𝜓))
41, 3bitr4i 267 1 ((𝐴 = 𝐵𝜓) ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382   = wceq 1632  wne 2932
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 197  df-or 384  df-ne 2933
This theorem is referenced by:  frsn  5346  ord0eln0  5940  fimaxre  11180  prime  11670  h1datomi  28770  elat2  29529  bnj563  31141  divrngidl  34158  dmncan1  34206  lkrshp4  34916  cvrcmp  35091  leat2  35102  isat3  35115  2llnmat  35331  2lnat  35591
  Copyright terms: Public domain W3C validator