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

Theorem neanior 2544
Description: A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
Assertion
Ref Expression
neanior  |-  ( ( A  =/=  B  /\  C  =/=  D )  <->  -.  ( A  =  B  \/  C  =  D )
)

Proof of Theorem neanior
StepHypRef Expression
1 df-ne 2461 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
2 df-ne 2461 . . 3  |-  ( C  =/=  D  <->  -.  C  =  D )
31, 2anbi12i 678 . 2  |-  ( ( A  =/=  B  /\  C  =/=  D )  <->  ( -.  A  =  B  /\  -.  C  =  D
) )
4 pm4.56 481 . 2  |-  ( ( -.  A  =  B  /\  -.  C  =  D )  <->  -.  ( A  =  B  \/  C  =  D )
)
53, 4bitri 240 1  |-  ( ( A  =/=  B  /\  C  =/=  D )  <->  -.  ( A  =  B  \/  C  =  D )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    \/ wo 357    /\ wa 358    = wceq 1632    =/= wne 2459
This theorem is referenced by:  nelpri  3674  0nelop  4272  om00  6589  om00el  6590  oeoe  6613  mulne0b  9425  xmulpnf1  10610  drngmulne0  15550  lvecvsn0  15878  domnmuln0  16055  abvn0b  16059  ply1domn  19525  vieta1lem1  19706  vieta1lem2  19707  atandm  20188  atandm3  20190  perfectlem2  20485  dchrelbas3  20493  nmlno0lem  21387  nmlnop0iALT  22591  chirredi  22990  mdsymi  23007  eldifpr  23409  subfacp1lem1  23725  vdgr1a  23912  neiopne  25154  fixpc  25197  filnetlem4  26433  isdomn3  27626  lcvbr3  29835  cvrnbtwn4  30091  elpadd0  30620  cdleme0moN  31036  cdleme0nex  31101
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-an 360  df-ne 2461
  Copyright terms: Public domain W3C validator