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

Theorem neanior 2728
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 2600 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
2 df-ne 2600 . . 3  |-  ( C  =/=  D  <->  -.  C  =  D )
31, 2anbi12i 695 . 2  |-  ( ( A  =/=  B  /\  C  =/=  D )  <->  ( -.  A  =  B  /\  -.  C  =  D
) )
4 pm4.56 493 . 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 366    /\ wa 367    = wceq 1405    =/= wne 2598
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 368  df-an 369  df-ne 2600
This theorem is referenced by:  eldifpr  3988  nelpri  3992  nelprd  3993  0nelop  4679  om00  7260  om00el  7261  oeoe  7284  mulne0b  10230  xmulpnf1  11518  drngmulne0  17736  lvecvsn0  18073  domnmuln0  18265  abvn0b  18269  mdetralt  19400  ply1domn  22814  vieta1lem1  22996  vieta1lem2  22997  atandm  23530  atandm3  23532  dchrelbas3  23892  vdgr1a  25310  nmlno0lem  26108  nmlnop0iALT  27313  chirredi  27712  subfacp1lem1  29463  filnetlem4  30596  lcvbr3  32021  cvrnbtwn4  32277  elpadd0  32806  cdleme0moN  33223  cdleme0nex  33288  isdomn3  35508  lcmgcd  36041  lcmdvds  36042  lidldomnnring  38228
  Copyright terms: Public domain W3C validator