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

Theorem neanior 3063
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 2972 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 df-ne 2972 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2anbi12i 621 . 2 ((𝐴𝐵𝐶𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4 pm4.56 1012 . 2 ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
53, 4bitri 267 1 ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 198  wa 385  wo 874   = wceq 1653  wne 2971
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 199  df-an 386  df-or 875  df-ne 2972
This theorem is referenced by:  nelpri  4393  nelprd  4395  eldifpr  4396  0nelop  5150  om00  7895  om00el  7896  oeoe  7919  mulne0b  10960  xmulpnf1  12353  lcmgcd  15655  lcmdvds  15656  drngmulne0  19087  lvecvsn0  19430  domnmuln0  19621  abvn0b  19625  mdetralt  20740  ply1domn  24224  vieta1lem1  24406  vieta1lem2  24407  atandm  24955  atandm3  24957  dchrelbas3  25315  eupth2lem3lem7  27579  frgrreg  27779  nmlno0lem  28173  nmlnop0iALT  29379  chirredi  29778  subfacp1lem1  31678  filnetlem4  32888  lcvbr3  35044  cvrnbtwn4  35300  elpadd0  35830  cdleme0moN  36246  cdleme0nex  36311  isdomn3  38567  lidldomnnring  42729
  Copyright terms: Public domain W3C validator