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

Theorem neneq 2947
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 2946 1 (𝐴𝐵 → ¬ 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wne 2941
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-ne 2942
This theorem is referenced by:  necon3ad  2954  necon3ai  2966  2reu4lem  4521  pr1eqbg  4853  disjprgw  5139  fpropnf1  7253  nf1const  7289  nelaneq  9581  gcd2n0cl  16437  lcmfunsnlem2lem1  16562  lcmfunsnlem2lem2  16563  ncoprmgcdne1b  16574  isnsgrp  18601  isnmnd  18616  mulmarep1gsum1  22044  fvmptnn04ifb  22322  tdeglem4  25546  isosctrlem2  26291  structiedg0val  28249  umgr2edgneu  28438  imadifxp  31798  f1resrcmplf1dlem  34020  aks6d1c2p2  40863  xppss12  40963  n0p  43601  supxrge  43921  uzn0bi  44042  elprn1  44222  elprn2  44223  liminflbuz2  44404  itgcoscmulx  44558  fourierdlem41  44737  elaa2  44823  sge0cl  44970  meadjiunlem  45054  hoidmvlelem2  45185  hspmbllem1  45215
  Copyright terms: Public domain W3C validator