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

Theorem neor 2651
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 360 . 2  |-  ( ( A  =  B  \/  ps )  <->  ( -.  A  =  B  ->  ps )
)
2 df-ne 2569 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
32imbi1i 316 . 2  |-  ( ( A  =/=  B  ->  ps )  <->  ( -.  A  =  B  ->  ps )
)
41, 3bitr4i 244 1  |-  ( ( A  =  B  \/  ps )  <->  ( A  =/= 
B  ->  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    = wceq 1649    =/= wne 2567
This theorem is referenced by:  fimaxre  9911  prime  10306  h1datomi  23036  elat2  23796  divrngidl  26528  dmncan1  26576  bnj563  28817  lkrshp4  29591  cvrcmp  29766  leat2  29777  isat3  29790  2llnmat  30006  2lnat  30266
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 178  df-or 360  df-ne 2569
  Copyright terms: Public domain W3C validator