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

Theorem neneq 2829
 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 2828 1 (𝐴𝐵 → ¬ 𝐴 = 𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = 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-ne 2824 This theorem is referenced by:  necon3ad  2836  pr1eqbg  4421  fpropnf1  6564  mpt2difsnif  6795  hash2prd  13295  fprodn0f  14766  gcd2n0cl  15278  lcmfunsnlem2lem1  15398  isnsgrp  17335  isnmnd  17345  structiedg0val  25956  umgr2edgneu  26151  clwwlknclwwlkdifsOLD  26947  numclwwlk3lemOLD  27369  n0p  39523  supxrge  39867  uzn0bi  40002  elprn1  40183  elprn2  40184  itgcoscmulx  40503  fourierdlem41  40683  elaa2  40769  sge0cl  40916  meadjiunlem  41000  hoidmvlelem2  41131  hspmbllem1  41161  2reu4a  41510  fdmdifeqresdif  42445
 Copyright terms: Public domain W3C validator