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

Theorem neanior 2915
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 2824 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 df-ne 2824 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2anbi12i 733 . 2 ((𝐴𝐵𝐶𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4 pm4.56 515 . 2 ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
53, 4bitri 264 1 ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wo 382  wa 383   = wceq 1523  wne 2823
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-or 384  df-an 385  df-ne 2824
This theorem is referenced by:  nelpri  4234  nelprd  4236  eldifpr  4237  0nelop  4989  om00  7700  om00el  7701  oeoe  7724  mulne0b  10706  xmulpnf1  12142  lcmgcd  15367  lcmdvds  15368  drngmulne0  18817  lvecvsn0  19157  domnmuln0  19346  abvn0b  19350  mdetralt  20462  ply1domn  23928  vieta1lem1  24110  vieta1lem2  24111  atandm  24648  atandm3  24650  dchrelbas3  25008  eupth2lem3lem7  27212  frgrreg  27381  nmlno0lem  27776  nmlnop0iALT  28982  chirredi  29381  subfacp1lem1  31287  filnetlem4  32501  lcvbr3  34628  cvrnbtwn4  34884  elpadd0  35413  cdleme0moN  35830  cdleme0nex  35895  isdomn3  38099  lidldomnnring  42255
  Copyright terms: Public domain W3C validator