Theorem neneq 2964

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 23	. 2 ⊢ (𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐵)
2	1	neneqd 2963	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ≠ wne 2958

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2959

This theorem is used by:  necon3ad  2971  necon3ai  2983  2reu4lem  4481  elprn1  4611  elprn2  4612  pr1eqbg  4814  fpropnf1  7278  f1resrcmplf1dlem  7285  nf1const  7319  nelaneqOLDOLD  9608  gcd2n0cl  16691  lcmfunsnlem2lem1  16825  lcmfunsnlem2lem2  16826  ncoprmgcdne1b  16837  isnsgrp  18924  isnmnd  18939  mulmarep1gsum1  22900  fvmptnn04ifb  23181  tdeglem4  26390  isosctrlem2  27159  nnsge1  28741  structiedg0val  29612  umgr2edgneu  29807  imadifxp  33249  elttcirr  37446  aks6d1c2p2  43309  xppss12  43423  n0p  46201  supxrge  46489  uzn0bi  46608  liminflbuz2  46964  itgcoscmulx  47118  fourierdlem41  47297  elaa2  47383  sge0cl  47530  meadjiunlem  47614  hoidmvlelem2  47745  hspmbllem1  47775  chnerlem1  48031