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

Theorem neor 2530
Description: Logical OR with an equality. (Contributed by NM, 29-Apr-2007.)
Assertion
Ref Expression
neor  |-  ( ( A  =  B  \/  ps )  <->  ( A  =/= 
B  ->  ps )
)

Proof of Theorem neor
StepHypRef Expression
1 df-or 359 . 2  |-  ( ( A  =  B  \/  ps )  <->  ( -.  A  =  B  ->  ps )
)
2 df-ne 2448 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
32imbi1i 315 . 2  |-  ( ( A  =/=  B  ->  ps )  <->  ( -.  A  =  B  ->  ps )
)
41, 3bitr4i 243 1  |-  ( ( A  =  B  \/  ps )  <->  ( A  =/= 
B  ->  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    = wceq 1623    =/= wne 2446
This theorem is referenced by:  fimaxre  9701  prime  10092  h1datomi  22160  elat2  22920  divrngidl  26653  dmncan1  26701  bnj563  28772  lkrshp4  29298  cvrcmp  29473  leat2  29484  isat3  29497  2llnmat  29713  2lnat  29973
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-ne 2448
  Copyright terms: Public domain W3C validator