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

Theorem neanior 3034
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 2941 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 df-ne 2941 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2anbi12i 628 . 2 ((𝐴𝐵𝐶𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4 pm4.56 988 . 2 ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
53, 4bitri 275 1 ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 397  wo 846   = wceq 1542  wne 2940
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 398  df-or 847  df-ne 2941
This theorem is referenced by:  nelpri  4616  nelprd  4618  eldifpr  4619  0nelop  5454  om00  8523  om00el  8524  oeoe  8547  mulne0b  11801  xmulpnf1  13199  lcmgcd  16488  lcmdvds  16489  drngmulne0  20223  lvecvsn0  20586  domnmuln0  20784  abvn0b  20788  mdetralt  21973  ply1domn  25504  vieta1lem1  25686  vieta1lem2  25687  atandm  26242  atandm3  26244  dchrelbas3  26602  eupth2lem3lem7  29220  frgrreg  29380  nmlno0lem  29777  nmlnop0iALT  30979  chirredi  31378  nelpr  31501  subfacp1lem1  33830  filnetlem4  34899  disjecxrn  36897  lcvbr3  37531  cvrnbtwn4  37787  elpadd0  38318  cdleme0moN  38734  cdleme0nex  38799  fsuppind  40808  isdomn3  41574  lidldomnnring  46314
  Copyright terms: Public domain W3C validator