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

Theorem neorian 3036
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 2943 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 df-ne 2943 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2orbi12i 879 . 2 ((𝐴𝐵𝐶𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷))
4 ianor 910 . 2 (¬ (𝐴 = 𝐵𝐶 = 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷))
53, 4bitr4i 267 1 ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 382  wo 826   = wceq 1630  wne 2942
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 197  df-an 383  df-or 827  df-ne 2943
This theorem is referenced by:  neneor  3041  oeoa  7830  wemapso2lem  8612  recextlem2  10859  crne0  11214  crreczi  13195  gcdcllem3  15430  bezoutlem2  15464  dsmmacl  20301  txhaus  21670  itg1addlem2  23683  coeaddlem  24224  dcubic  24793  sibfof  30736  nrhmzr  42391
  Copyright terms: Public domain W3C validator