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

Theorem neor 3034
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 846 . 2 ((𝐴 = 𝐵𝜓) ↔ (¬ 𝐴 = 𝐵𝜓))
2 df-ne 2941 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
32imbi1i 349 . 2 ((𝐴𝐵𝜓) ↔ (¬ 𝐴 = 𝐵𝜓))
41, 3bitr4i 277 1 ((𝐴 = 𝐵𝜓) ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wo 845   = wceq 1541  wne 2940
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 206  df-or 846  df-ne 2941
This theorem is referenced by:  frsn  5763  ord0eln0  6419  fimaxre  12157  fiminre  12160  prime  12642  h1datomi  30829  elat2  31588  bnj563  33749  divrngidl  36891  dmncan1  36939  lkrshp4  37973  cvrcmp  38148  leat2  38159  isat3  38172  2llnmat  38390  2lnat  38650
  Copyright terms: Public domain W3C validator