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

Theorem neanior 3037
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 627 . 2 ((𝐴𝐵𝐶𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4 pm4.56 986 . 2 ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
53, 4bitri 274 1 ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 396  wo 844   = wceq 1539  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 206  df-an 397  df-or 845  df-ne 2944
This theorem is referenced by:  nelpri  4590  nelprd  4592  eldifpr  4593  0nelop  5410  om00  8406  om00el  8407  oeoe  8430  mulne0b  11616  xmulpnf1  13008  lcmgcd  16312  lcmdvds  16313  drngmulne0  20013  lvecvsn0  20371  domnmuln0  20569  abvn0b  20573  mdetralt  21757  ply1domn  25288  vieta1lem1  25470  vieta1lem2  25471  atandm  26026  atandm3  26028  dchrelbas3  26386  eupth2lem3lem7  28598  frgrreg  28758  nmlno0lem  29155  nmlnop0iALT  30357  chirredi  30756  nelpr  30879  subfacp1lem1  33141  filnetlem4  34570  lcvbr3  37037  cvrnbtwn4  37293  elpadd0  37823  cdleme0moN  38239  cdleme0nex  38304  fsuppind  40279  isdomn3  41029  lidldomnnring  45488
  Copyright terms: Public domain W3C validator