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

Theorem neor 3108
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 842 . 2 ((𝐴 = 𝐵𝜓) ↔ (¬ 𝐴 = 𝐵𝜓))
2 df-ne 3017 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
32imbi1i 351 . 2 ((𝐴𝐵𝜓) ↔ (¬ 𝐴 = 𝐵𝜓))
41, 3bitr4i 279 1 ((𝐴 = 𝐵𝜓) ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wo 841   = wceq 1528  wne 3016
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 208  df-or 842  df-ne 3017
This theorem is referenced by:  frsn  5633  ord0eln0  6239  fimaxre  11573  fimaxreOLD  11574  fiminre  11577  prime  12052  h1datomi  29286  elat2  30045  bnj563  31914  divrngidl  35189  dmncan1  35237  lkrshp4  36126  cvrcmp  36301  leat2  36312  isat3  36325  2llnmat  36542  2lnat  36802
  Copyright terms: Public domain W3C validator