Theorem neneq 2963

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1560   ≠ wne 2957

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 209  df-ne 2958

This theorem is referenced by:  necon3ad  2970  necon3ai  2982  2reu4lem  4477  elprn1  4610  elprn2  4611  pr1eqbg  4815  fpropnf1  7251  nf1const  7288  nelaneqOLDOLD  9552  gcd2n0cl  16543  lcmfunsnlem2lem1  16672  lcmfunsnlem2lem2  16673  ncoprmgcdne1b  16684  isnsgrp  18757  isnmnd  18772  mulmarep1gsum1  22633  fvmptnn04ifb  22911  tdeglem4  26120  isosctrlem2  26884  nnsge1  28436  structiedg0val  29223  umgr2edgneu  29415  imadifxp  32801  f1resrcmplf1dlem  35380  elttcirr  36891  aks6d1c2p2  42736  xppss12  42848  n0p  45625  supxrge  45914  uzn0bi  46033  liminflbuz2  46389  itgcoscmulx  46543  fourierdlem41  46722  elaa2  46808  sge0cl  46955  meadjiunlem  47039  hoidmvlelem2  47170  hspmbllem1  47200  chnerlem1  47458