Theorem neneq 2948

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 2947	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942

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 2943

This theorem is referenced by:  necon3ad  2955  necon3ai  2967  2reu4lem  4453  pr1eqbg  4784  disjprgw  5065  fpropnf1  7121  nf1const  7156  nelaneq  9288  gcd2n0cl  16144  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  ncoprmgcdne1b  16283  isnsgrp  18294  isnmnd  18304  mulmarep1gsum1  21630  fvmptnn04ifb  21908  tdeglem4  25129  isosctrlem2  25874  structiedg0val  27295  umgr2edgneu  27484  imadifxp  30841  f1resrcmplf1dlem  32958  xppss12  40130  n0p  42480  supxrge  42767  uzn0bi  42889  elprn1  43064  elprn2  43065  liminflbuz2  43246  itgcoscmulx  43400  fourierdlem41  43579  elaa2  43665  sge0cl  43809  meadjiunlem  43893  hoidmvlelem2  44024  hspmbllem1  44054