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 2941 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 df-ne 2941 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2orbi12i 914 . 2 ((𝐴𝐵𝐶𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷))
4 ianor 981 . 2 (¬ (𝐴 = 𝐵𝐶 = 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷))
53, 4bitr4i 278 1 ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 397  wo 846   = wceq 1542  wne 2940
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 206  df-an 398  df-or 847  df-ne 2941
This theorem is referenced by:  neneor  3041  poxp2  8076  oeoa  8545  recextlem2  11791  crne0  12151  crreczi  14137  gcdcllem3  16386  bezoutlem2  16426  dsmmacl  21163  mhpmulcl  21555  txhaus  23014  itg1addlem2  25077  coeaddlem  25626  dcubic  26212  creq0  31699  sibfof  32997  nrhmzr  46257  rrx2pnecoorneor  46887
  Copyright terms: Public domain W3C validator