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

Theorem neanior 3114
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 3022 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 df-ne 3022 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2anbi12i 626 . 2 ((𝐴𝐵𝐶𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4 pm4.56 984 . 2 ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
53, 4bitri 276 1 ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wa 396  wo 843   = wceq 1530  wne 3021
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 208  df-an 397  df-or 844  df-ne 3022
This theorem is referenced by:  nelpri  4591  nelprd  4593  eldifpr  4594  0nelop  5383  om00  8191  om00el  8192  oeoe  8215  mulne0b  11270  xmulpnf1  12657  lcmgcd  15941  lcmdvds  15942  drngmulne0  19444  lvecvsn0  19801  domnmuln0  19990  abvn0b  19994  mdetralt  21133  ply1domn  24632  vieta1lem1  24814  vieta1lem2  24815  atandm  25367  atandm3  25369  dchrelbas3  25728  eupth2lem3lem7  27927  frgrreg  28087  nmlno0lem  28484  nmlnop0iALT  29686  chirredi  30085  nelpr  30205  subfacp1lem1  32310  filnetlem4  33613  lcvbr3  36026  cvrnbtwn4  36282  elpadd0  36812  cdleme0moN  37228  cdleme0nex  37293  isdomn3  39669  lidldomnnring  44033
  Copyright terms: Public domain W3C validator