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

Theorem neanior 2695
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 2606 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
2 df-ne 2606 . . 3  |-  ( C  =/=  D  <->  -.  C  =  D )
31, 2anbi12i 692 . 2  |-  ( ( A  =/=  B  /\  C  =/=  D )  <->  ( -.  A  =  B  /\  -.  C  =  D
) )
4 pm4.56 492 . 2  |-  ( ( -.  A  =  B  /\  -.  C  =  D )  <->  -.  ( A  =  B  \/  C  =  D )
)
53, 4bitri 249 1  |-  ( ( A  =/=  B  /\  C  =/=  D )  <->  -.  ( A  =  B  \/  C  =  D )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1364    =/= wne 2604
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 2606
This theorem is referenced by:  eldifpr  3891  nelpri  3895  nelprd  3896  0nelop  4578  om00  7010  om00el  7011  oeoe  7034  mulne0b  9973  xmulpnf1  11233  drngmulne0  16834  lvecvsn0  17168  domnmuln0  17348  abvn0b  17352  mdetralt  18373  ply1domn  21554  vieta1lem1  21735  vieta1lem2  21736  atandm  22230  atandm3  22232  perfectlem2  22528  dchrelbas3  22536  vdgr1a  23511  nmlno0lem  24128  nmlnop0iALT  25334  chirredi  25733  mdsymi  25750  subfacp1lem1  26997  filnetlem4  28527  isdomn3  29497  lcvbr3  32390  cvrnbtwn4  32646  elpadd0  33175  cdleme0moN  33591  cdleme0nex  33656
  Copyright terms: Public domain W3C validator