Theorem neneq 2938

Description: From inequality to non-equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
neneq	⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)

Proof of Theorem neneq

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐵)
2	1	neneqd 2937	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1543   ≠ wne 2932

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 2933

This theorem is referenced by:  necon3ad  2945  2reu4lem  4423  pr1eqbg  4753  disjprgw  5034  fpropnf1  7057  nf1const  7092  nelaneq  9193  gcd2n0cl  16031  lcmfunsnlem2lem1  16158  lcmfunsnlem2lem2  16159  ncoprmgcdne1b  16170  isnsgrp  18121  isnmnd  18131  mulmarep1gsum1  21424  fvmptnn04ifb  21702  tdeglem4  24911  isosctrlem2  25656  structiedg0val  27067  umgr2edgneu  27256  imadifxp  30613  f1resrcmplf1dlem  32725  xppss12  39858  n0p  42205  supxrge  42491  uzn0bi  42615  elprn1  42792  elprn2  42793  liminflbuz2  42974  itgcoscmulx  43128  fourierdlem41  43307  elaa2  43393  sge0cl  43537  meadjiunlem  43621  hoidmvlelem2  43752  hspmbllem1  43782