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

Theorem neorian 3111
Description: A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
Assertion
Ref Expression
neorian ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))

Proof of Theorem neorian
StepHypRef Expression
1 df-ne 3017 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 df-ne 3017 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2orbi12i 908 . 2 ((𝐴𝐵𝐶𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷))
4 ianor 975 . 2 (¬ (𝐴 = 𝐵𝐶 = 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷))
53, 4bitr4i 279 1 ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wa 396  wo 841   = wceq 1528  wne 3016
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 208  df-an 397  df-or 842  df-ne 3017
This theorem is referenced by:  neneor  3118  oeoa  8213  recextlem2  11260  crne0  11620  crreczi  13579  gcdcllem3  15840  bezoutlem2  15878  dsmmacl  20815  txhaus  22185  itg1addlem2  24227  coeaddlem  24768  dcubic  25351  creq0  30398  sibfof  31498  nrhmzr  44042  rrx2pnecoorneor  44600
  Copyright terms: Public domain W3C validator