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

Theorem neanior 2792
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 2664 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
2 df-ne 2664 . . 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 1379    =/= wne 2662
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 2664
This theorem is referenced by:  eldifpr  4044  nelpri  4048  nelprd  4049  0nelop  4737  om00  7221  om00el  7222  oeoe  7245  mulne0b  10186  xmulpnf1  11462  drngmulne0  17201  lvecvsn0  17538  domnmuln0  17718  abvn0b  17722  mdetralt  18877  ply1domn  22259  vieta1lem1  22440  vieta1lem2  22441  atandm  22935  atandm3  22937  perfectlem2  23233  dchrelbas3  23241  vdgr1a  24582  nmlno0lem  25384  nmlnop0iALT  26590  chirredi  26989  mdsymi  27006  subfacp1lem1  28263  filnetlem4  29802  isdomn3  30769  lcmgcd  30813  lcmdvds  30814  lcvbr3  33820  cvrnbtwn4  34076  elpadd0  34605  cdleme0moN  35021  cdleme0nex  35086
  Copyright terms: Public domain W3C validator