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

Theorem neor 2543
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 2461 . . 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 1632    =/= wne 2459
This theorem is referenced by:  fimaxre  9717  prime  10108  h1datomi  22176  elat2  22936  divrngidl  26756  dmncan1  26804  bnj563  29088  lkrshp4  29920  cvrcmp  30095  leat2  30106  isat3  30119  2llnmat  30335  2lnat  30595
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 2461
  Copyright terms: Public domain W3C validator