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

Theorem neanior 2531
Description: A DeMorgan'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 2448 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
2 df-ne 2448 . . 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 1623    =/= wne 2446
This theorem is referenced by:  nelpri  3661  0nelop  4256  om00  6573  om00el  6574  oeoe  6597  mulne0b  9409  xmulpnf1  10594  drngmulne0  15534  lvecvsn0  15862  domnmuln0  16039  abvn0b  16043  ply1domn  19509  vieta1lem1  19690  vieta1lem2  19691  atandm  20172  atandm3  20174  perfectlem2  20469  dchrelbas3  20477  nmlno0lem  21371  nmlnop0iALT  22575  chirredi  22974  mdsymi  22991  eldifpr  23394  subfacp1lem1  23710  vdgr1a  23897  neiopne  25051  fixpc  25094  filnetlem4  26330  isdomn3  27523  lcvbr3  29213  cvrnbtwn4  29469  elpadd0  29998  cdleme0moN  30414  cdleme0nex  30479
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 2448
  Copyright terms: Public domain W3C validator