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

Theorem neorian 3109
 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 3015 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 df-ne 3015 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2orbi12i 910 . 2 ((𝐴𝐵𝐶𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷))
4 ianor 977 . 2 (¬ (𝐴 = 𝐵𝐶 = 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷))
53, 4bitr4i 280 1 ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 398   ∨ wo 843   = wceq 1530   ≠ wne 3014 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 209  df-an 399  df-or 844  df-ne 3015 This theorem is referenced by:  neneor  3116  oeoa  8215  recextlem2  11263  crne0  11623  crreczi  13581  gcdcllem3  15842  bezoutlem2  15880  dsmmacl  20877  txhaus  22247  itg1addlem2  24290  coeaddlem  24831  dcubic  25416  creq0  30463  sibfof  31586  nrhmzr  44129  rrx2pnecoorneor  44687
 Copyright terms: Public domain W3C validator