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

Theorem neor 2688
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 2601 . . 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 1652    =/= wne 2599
This theorem is referenced by:  fimaxre  9955  prime  10350  h1datomi  23083  elat2  23843  divrngidl  26638  dmncan1  26686  bnj563  29111  lkrshp4  29906  cvrcmp  30081  leat2  30092  isat3  30105  2llnmat  30321  2lnat  30581
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 2601
  Copyright terms: Public domain W3C validator