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

Theorem neanior 3027
Description: A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
Assertion
Ref Expression
neanior ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))

Proof of Theorem neanior
StepHypRef Expression
1 df-ne 2936 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 df-ne 2936 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2anbi12i 630 . 2 ((𝐴𝐵𝐶𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4 pm4.56 988 . 2 ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
53, 4bitri 278 1 ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wa 399  wo 846   = wceq 1542  wne 2935
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 210  df-an 400  df-or 847  df-ne 2936
This theorem is referenced by:  nelpri  4555  nelprd  4557  eldifpr  4558  0nelop  5363  om00  8244  om00el  8245  oeoe  8268  mulne0b  11371  xmulpnf1  12762  lcmgcd  16060  lcmdvds  16061  drngmulne0  19655  lvecvsn0  20012  domnmuln0  20202  abvn0b  20206  mdetralt  21371  ply1domn  24888  vieta1lem1  25070  vieta1lem2  25071  atandm  25626  atandm3  25628  dchrelbas3  25986  eupth2lem3lem7  28183  frgrreg  28343  nmlno0lem  28740  nmlnop0iALT  29942  chirredi  30341  nelpr  30465  subfacp1lem1  32724  filnetlem4  34225  lcvbr3  36692  cvrnbtwn4  36948  elpadd0  37478  cdleme0moN  37894  cdleme0nex  37959  fsuppind  39898  isdomn3  40641  lidldomnnring  45069
  Copyright terms: Public domain W3C validator