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

Theorem neanior 2689
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 2601 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
2 df-ne 2601 . . 3  |-  ( C  =/=  D  <->  -.  C  =  D )
31, 2anbi12i 679 . 2  |-  ( ( A  =/=  B  /\  C  =/=  D )  <->  ( -.  A  =  B  /\  -.  C  =  D
) )
4 pm4.56 482 . 2  |-  ( ( -.  A  =  B  /\  -.  C  =  D )  <->  -.  ( A  =  B  \/  C  =  D )
)
53, 4bitri 241 1  |-  ( ( A  =/=  B  /\  C  =/=  D )  <->  -.  ( A  =  B  \/  C  =  D )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    \/ wo 358    /\ wa 359    = wceq 1652    =/= wne 2599
This theorem is referenced by:  nelpri  3835  0nelop  4446  om00  6818  om00el  6819  oeoe  6842  mulne0b  9663  xmulpnf1  10853  drngmulne0  15857  lvecvsn0  16181  domnmuln0  16358  abvn0b  16362  ply1domn  20046  vieta1lem1  20227  vieta1lem2  20228  atandm  20716  atandm3  20718  perfectlem2  21014  dchrelbas3  21022  vdgr1a  21677  nmlno0lem  22294  nmlnop0iALT  23498  chirredi  23897  mdsymi  23914  eldifpr  24392  subfacp1lem1  24865  filnetlem4  26410  isdomn3  27500  nelprd  28055  lcvbr3  29821  cvrnbtwn4  30077  elpadd0  30606  cdleme0moN  31022  cdleme0nex  31087
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 178  df-or 360  df-an 361  df-ne 2601
  Copyright terms: Public domain W3C validator