MPE Home 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