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

Theorem neor 2781
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 370 . 2
2 df-ne 2654 . . 3
32imbi1i 325 . 2
41, 3bitr4i 252 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  =wceq 1395  =/=wne 2652
This theorem is referenced by:  fimaxre  10515  prime  10968  h1datomi  26499  elat2  27259  divrngidl  30425  dmncan1  30473  bnj563  33800  lkrshp4  34833  cvrcmp  35008  leat2  35019  isat3  35032  2llnmat  35248  2lnat  35508
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 185  df-or 370  df-ne 2654
  Copyright terms: Public domain W3C validator