Theorem neneq 2945

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

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

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 2940

This theorem is referenced by:  necon3ad  2952  necon3ai  2964  2reu4lem  4521  pr1eqbg  4856  fpropnf1  7288  nf1const  7325  nelaneq  9640  gcd2n0cl  16547  lcmfunsnlem2lem1  16676  lcmfunsnlem2lem2  16677  ncoprmgcdne1b  16688  isnsgrp  18737  isnmnd  18752  mulmarep1gsum1  22580  fvmptnn04ifb  22858  tdeglem4  26100  isosctrlem2  26863  nnsge1  28347  structiedg0val  29040  umgr2edgneu  29232  imadifxp  32615  f1resrcmplf1dlem  35101  aks6d1c2p2  42121  xppss12  42269  n0p  45055  supxrge  45354  uzn0bi  45475  elprn1  45653  elprn2  45654  liminflbuz2  45835  itgcoscmulx  45989  fourierdlem41  46168  elaa2  46254  sge0cl  46401  meadjiunlem  46485  hoidmvlelem2  46616  hspmbllem1  46646