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

Theorem neneq 2996
 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 2995 1 (𝐴𝐵 → ¬ 𝐴 = 𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2990 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 210  df-ne 2991 This theorem is referenced by:  necon3ad  3003  2reu4lem  4426  pr1eqbg  4750  disjprgw  5028  fpropnf1  7007  nf1const  7042  nelaneq  9051  gcd2n0cl  15852  lcmfunsnlem2lem1  15976  lcmfunsnlem2lem2  15977  ncoprmgcdne1b  15988  isnsgrp  17901  isnmnd  17911  mulmarep1gsum1  21182  fvmptnn04ifb  21460  isosctrlem2  25409  structiedg0val  26819  umgr2edgneu  27008  imadifxp  30368  f1resrcmplf1dlem  32473  xppss12  39402  n0p  41670  supxrge  41963  uzn0bi  42091  elprn1  42268  elprn2  42269  liminflbuz2  42450  itgcoscmulx  42604  fourierdlem41  42783  elaa2  42869  sge0cl  43013  meadjiunlem  43097  hoidmvlelem2  43228  hspmbllem1  43258
 Copyright terms: Public domain W3C validator