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

Theorem neanior 2874
 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 2782 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 df-ne 2782 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2anbi12i 729 . 2 ((𝐴𝐵𝐶𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4 pm4.56 515 . 2 ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
53, 4bitri 263 1 ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ≠ wne 2780 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 196  df-or 384  df-an 385  df-ne 2782 This theorem is referenced by:  nelpri  4149  nelprd  4151  eldifpr  4152  0nelop  4886  om00  7542  om00el  7543  oeoe  7566  mulne0b  10547  xmulpnf1  11976  lcmgcd  15158  lcmdvds  15159  drngmulne0  18592  lvecvsn0  18930  domnmuln0  19119  abvn0b  19123  mdetralt  20233  ply1domn  23687  vieta1lem1  23869  vieta1lem2  23870  atandm  24403  atandm3  24405  dchrelbas3  24763  vdgr1a  26433  nmlno0lem  27032  nmlnop0iALT  28238  chirredi  28637  subfacp1lem1  30415  filnetlem4  31546  lcvbr3  33328  cvrnbtwn4  33584  elpadd0  34113  cdleme0moN  34530  cdleme0nex  34595  isdomn3  36801  eupth2lem3lem7  41402  av-frgrareg  41548  lidldomnnring  41720
 Copyright terms: Public domain W3C validator