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

Theorem neorian 2749
Description: A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
Assertion
Ref Expression
neorian  |-  ( ( A  =/=  B  \/  C  =/=  D )  <->  -.  ( A  =  B  /\  C  =  D )
)

Proof of Theorem neorian
StepHypRef Expression
1 df-ne 2618 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
2 df-ne 2618 . . 3  |-  ( C  =/=  D  <->  -.  C  =  D )
31, 2orbi12i 523 . 2  |-  ( ( A  =/=  B  \/  C  =/=  D )  <->  ( -.  A  =  B  \/  -.  C  =  D
) )
4 ianor 490 . 2  |-  ( -.  ( A  =  B  /\  C  =  D )  <->  ( -.  A  =  B  \/  -.  C  =  D )
)
53, 4bitr4i 255 1  |-  ( ( A  =/=  B  \/  C  =/=  D )  <->  -.  ( A  =  B  /\  C  =  D )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187    \/ wo 369    /\ wa 370    = wceq 1437    =/= wne 2616
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 188  df-or 371  df-an 372  df-ne 2618
This theorem is referenced by:  neneor  2753  oeoa  7297  wemapso2lem  8058  recextlem2  10232  crne0  10591  crreczi  12383  gcdcllem3  14438  bezoutlem2  14467  dsmmacl  19241  txhaus  20599  itg1addlem2  22562  coeaddlem  23110  dcubic  23676  sibfof  29042  nrhmzr  38688
  Copyright terms: Public domain W3C validator