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

Theorem neanior 3035
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 2944 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 df-ne 2944 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2anbi12i 612 . 2 ((𝐴𝐵𝐶𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4 pm4.56 973 . 2 ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
53, 4bitri 264 1 ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 382  wo 836   = wceq 1631  wne 2943
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 197  df-an 383  df-or 837  df-ne 2944
This theorem is referenced by:  nelpri  4341  nelprd  4343  eldifpr  4344  0nelop  5088  om00  7813  om00el  7814  oeoe  7837  mulne0b  10874  xmulpnf1  12309  lcmgcd  15528  lcmdvds  15529  drngmulne0  18979  lvecvsn0  19322  domnmuln0  19513  abvn0b  19517  mdetralt  20632  ply1domn  24103  vieta1lem1  24285  vieta1lem2  24286  atandm  24824  atandm3  24826  dchrelbas3  25184  eupth2lem3lem7  27414  frgrreg  27593  nmlno0lem  27988  nmlnop0iALT  29194  chirredi  29593  subfacp1lem1  31499  filnetlem4  32713  lcvbr3  34830  cvrnbtwn4  35086  elpadd0  35616  cdleme0moN  36033  cdleme0nex  36098  isdomn3  38306  lidldomnnring  42453
  Copyright terms: Public domain W3C validator