MPE Home 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