Theorem neneq 2965

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

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

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 2960

This theorem is used by:  necon3ad  2972  necon3ai  2984  2reu4lem  4482  elprn1  4612  elprn2  4613  pr1eqbg  4817  fpropnf1  7302  f1resrcmplf1dlem  7309  nf1const  7343  nelaneqOLDOLD  9635  gcd2n0cl  16723  lcmfunsnlem2lem1  16857  lcmfunsnlem2lem2  16858  ncoprmgcdne1b  16869  isnsgrp  18962  isnmnd  18977  mulmarep1gsum1  22943  fvmptnn04ifb  23224  tdeglem4  26433  isosctrlem2  27204  nnsge1  28786  structiedg0val  29657  umgr2edgneu  29852  imadifxp  33293  elttcirr  37534  aks6d1c2p2  43435  xppss12  43550  n0p  46336  supxrge  46623  uzn0bi  46742  liminflbuz2  47098  itgcoscmulx  47252  fourierdlem41  47431  elaa2  47517  sge0cl  47664  meadjiunlem  47748  hoidmvlelem2  47879  hspmbllem1  47909  chnerlem1  48165