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

Theorem neorian 2784
Description: A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
Assertion
Ref Expression
neorian

Proof of Theorem neorian
StepHypRef Expression
1 df-ne 2654 . . 3
2 df-ne 2654 . . 3
31, 2orbi12i 521 . 2
4 ianor 488 . 2
53, 4bitr4i 252 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  \/wo 368  /\wa 369  =wceq 1395  =/=wne 2652
This theorem is referenced by:  oeoa  7265  wemapso2OLD  7998  wemapso2lem  7999  recextlem2  10205  crne0  10554  crreczi  12291  gcdcllem3  14151  bezoutlem2  14177  dsmmacl  18772  txhaus  20148  itg1addlem2  22104  coeaddlem  22646  dcubic  23177  sibfof  28282  nrhmzr  32679
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-an 371  df-ne 2654
  Copyright terms: Public domain W3C validator