Theorem neneq 2961

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

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

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 2956

This theorem is used by:  necon3ad  2968  necon3ai  2980  2reu4lem  4479  elprn1  4612  elprn2  4613  pr1eqbg  4817  fpropnf1  7265  f1resrcmplf1dlem  7272  nf1const  7306  nelaneqOLDOLD  9577  gcd2n0cl  16600  lcmfunsnlem2lem1  16729  lcmfunsnlem2lem2  16730  ncoprmgcdne1b  16741  isnsgrp  18826  isnmnd  18841  mulmarep1gsum1  22796  fvmptnn04ifb  23077  tdeglem4  26286  isosctrlem2  27057  nnsge1  28609  structiedg0val  29480  umgr2edgneu  29675  imadifxp  33075  elttcirr  37151  aks6d1c2p2  42986  xppss12  43100  n0p  45880  supxrge  46169  uzn0bi  46288  liminflbuz2  46644  itgcoscmulx  46798  fourierdlem41  46977  elaa2  47063  sge0cl  47210  meadjiunlem  47294  hoidmvlelem2  47425  hspmbllem1  47455  chnerlem1  47711