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

Theorem neneq 2788
 Description: From inequality to non equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Assertion
Ref Expression
neneq (𝐴𝐵 → ¬ 𝐴 = 𝐵)

Proof of Theorem neneq
StepHypRef Expression
1 id 22 . 2 (𝐴𝐵𝐴𝐵)
21neneqd 2787 1 (𝐴𝐵 → ¬ 𝐴 = 𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = 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-ne 2782 This theorem is referenced by:  necon3ad  2795  nelsnOLD  4160  hash2prd  13114  fprodn0f  14561  gcd2n0cl  15069  lcmfunsnlem2lem1  15189  structiedg0val  25699  n0p  38234  supxrge  38495  elprn1  38700  elprn2  38701  itgcoscmulx  38861  fourierdlem41  39041  elaa2  39127  sge0cl  39274  meadjiunlem  39358  hoidmvlelem2  39486  hspmbllem1  39516  fpropnf1  40337  umgr2edgneu  40441  clwwlknclwwlkdifs  41181  av-numclwwlk3lem  41538
 Copyright terms: Public domain W3C validator