Theorem neneq 2966

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

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

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 2961

This theorem is used by:  necon3ad  2973  necon3ai  2985  2reu4lem  4486  elprn1  4619  elprn2  4620  pr1eqbg  4824  fpropnf1  7270  f1resrcmplf1dlem  7277  nf1const  7311  nelaneqOLDOLD  9573  gcd2n0cl  16591  lcmfunsnlem2lem1  16720  lcmfunsnlem2lem2  16721  ncoprmgcdne1b  16732  isnsgrp  18815  isnmnd  18830  mulmarep1gsum1  22782  fvmptnn04ifb  23060  tdeglem4  26270  isosctrlem2  27037  nnsge1  28589  structiedg0val  29429  umgr2edgneu  29624  imadifxp  33019  elttcirr  37101  aks6d1c2p2  42946  xppss12  43060  n0p  45825  supxrge  46114  uzn0bi  46233  liminflbuz2  46589  itgcoscmulx  46743  fourierdlem41  46922  elaa2  47008  sge0cl  47155  meadjiunlem  47239  hoidmvlelem2  47370  hspmbllem1  47400  chnerlem1  47658