Theorem neneq 2932

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2926

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 207  df-ne 2927

This theorem is referenced by:  necon3ad  2939  necon3ai  2951  2reu4lem  4488  pr1eqbg  4824  fpropnf1  7245  nf1const  7282  nelaneq  9559  gcd2n0cl  16486  lcmfunsnlem2lem1  16615  lcmfunsnlem2lem2  16616  ncoprmgcdne1b  16627  isnsgrp  18657  isnmnd  18672  mulmarep1gsum1  22467  fvmptnn04ifb  22745  tdeglem4  25972  isosctrlem2  26736  nnsge1  28242  structiedg0val  28956  umgr2edgneu  29148  imadifxp  32537  f1resrcmplf1dlem  35083  aks6d1c2p2  42114  xppss12  42224  n0p  45046  supxrge  45341  uzn0bi  45462  elprn1  45638  elprn2  45639  liminflbuz2  45820  itgcoscmulx  45974  fourierdlem41  46153  elaa2  46239  sge0cl  46386  meadjiunlem  46470  hoidmvlelem2  46601  hspmbllem1  46631