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

Theorem neorian 3026
 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 2933 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 df-ne 2933 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2orbi12i 544 . 2 ((𝐴𝐵𝐶𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷))
4 ianor 510 . 2 (¬ (𝐴 = 𝐵𝐶 = 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷))
53, 4bitr4i 267 1 ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 196   ∨ wo 382   ∧ wa 383   = wceq 1632   ≠ wne 2932 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-or 384  df-an 385  df-ne 2933 This theorem is referenced by:  neneor  3031  oeoa  7846  wemapso2lem  8622  recextlem2  10850  crne0  11205  crreczi  13183  gcdcllem3  15425  bezoutlem2  15459  dsmmacl  20287  txhaus  21652  itg1addlem2  23663  coeaddlem  24204  dcubic  24772  sibfof  30711  nrhmzr  42383
 Copyright terms: Public domain W3C validator