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

Theorem neanior 2702
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 2613 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
2 df-ne 2613 . . 3  |-  ( C  =/=  D  <->  -.  C  =  D )
31, 2anbi12i 697 . 2  |-  ( ( A  =/=  B  /\  C  =/=  D )  <->  ( -.  A  =  B  /\  -.  C  =  D
) )
4 pm4.56 495 . 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 1369    =/= wne 2611
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 2613
This theorem is referenced by:  eldifpr  3899  nelpri  3903  nelprd  3904  0nelop  4586  om00  7019  om00el  7020  oeoe  7043  mulne0b  9982  xmulpnf1  11242  drngmulne0  16859  lvecvsn0  17195  domnmuln0  17375  abvn0b  17379  mdetralt  18419  ply1domn  21600  vieta1lem1  21781  vieta1lem2  21782  atandm  22276  atandm3  22278  perfectlem2  22574  dchrelbas3  22582  vdgr1a  23581  nmlno0lem  24198  nmlnop0iALT  25404  chirredi  25803  mdsymi  25820  subfacp1lem1  27072  filnetlem4  28607  isdomn3  29577  lcvbr3  32673  cvrnbtwn4  32929  elpadd0  33458  cdleme0moN  33874  cdleme0nex  33939
  Copyright terms: Public domain W3C validator