Theorem neqne 2934

Description: From non-equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
neqne	⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵)

Proof of Theorem neqne

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (¬ 𝐴 = 𝐵 → ¬ 𝐴 = 𝐵)
2	1	neqned 2933	1 ⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2926

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 207  df-ne 2927

This theorem is referenced by:  exmidne  2936  domwdom  9534  epnsym  9569  dfac2b  10091  fin23lem14  10293  axcc2lem  10396  fiminre2  12138  cshw1  14794  xptrrel  14953  dvdsabseq  16290  ncoprmgcdne1b  16627  sgrp2rid2  18860  symg2bas  19330  symgextf  19354  odlem1  19472  gexlem1  19516  ablsimpgfind  20049  psgndiflemB  21516  cply1mul  22190  dmatmul  22391  mdetdiag  22493  mdetunilem9  22514  maducoeval2  22534  madurid  22538  chfacfisf  22748  chfacfisfcpmat  22749  plyexmo  26228  aalioulem3  26249  dvradcnv  26337  logtayllem  26575  logtayl  26576  upgriswlk  29576  lfgrwlkprop  29622  2pthnloop  29668  umgr2adedgspth  29885  umgrclwwlkge2  29927  n4cyclfrgr  30227  frgrwopreglem3  30250  frgrregorufr0  30260  domnmuln0rd  33232  elrspunsn  33407  satfv1lem  35356  bj-rest10b  37084  aks6d1c2p2  42114  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  aks6d1c6lem3  42167  aks6d1c7  42179  unitscyglem2  42191  xppss12  42224  sn-0tie0  42446  prjspnfv01  42619  prjspner01  42620  fiiuncl  45066  disjf1  45184  fzisoeu  45305  fzdifsuc2  45315  supxrge  45341  suplesup  45342  infrpge  45354  xrlexaddrp  45355  infleinflem1  45373  infleinflem2  45374  infleinf  45375  xralrple3  45377  xrralrecnnge  45393  infxrpnf  45449  supminfxr  45467  fsumsupp0  45583  limcresiooub  45647  limcresioolb  45648  limclr  45660  climisp  45751  climxlim2lem  45850  dfxlim2v  45852  xlimliminflimsup  45867  icccncfext  45892  cncfiooiccre  45900  dvbdfbdioolem2  45934  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnxpaek  45947  dvnprodlem3  45953  itgioocnicc  45982  ovolsplit  45993  stoweidlem14  46019  stoweidlem55  46060  stoweid  46068  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkercncf  46112  fourierdlem9  46121  fourierdlem30  46142  fourierdlem31  46143  fourierdlem33  46145  fourierdlem34  46146  fourierdlem35  46147  fourierdlem42  46154  fourierdlem43  46155  fourierdlem46  46157  fourierdlem48  46159  fourierdlem49  46160  fourierdlem51  46162  fourierdlem54  46165  fourierdlem62  46173  fourierdlem64  46175  fourierdlem65  46176  fourierdlem70  46181  fourierdlem71  46182  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem79  46190  fourierdlem81  46192  fourierdlem82  46193  fourierdlem89  46200  fourierdlem91  46202  fourierdlem102  46213  fourierdlem114  46225  sqwvfoura  46233  fourierswlem  46235  fouriersw  46236  elaa2lem  46238  etransclem25  46264  etransclem28  46267  etransclem35  46274  etransclem38  46277  qndenserrnbl  46300  ioorrnopn  46310  ioorrnopnxrlem  46311  ioorrnopnxr  46312  prsal  46323  issalnnd  46350  sge0cl  46386  sge0pr  46399  sge0prle  46406  sge0isum  46432  sge0xaddlem1  46438  iundjiun  46465  meadjun  46467  ismeannd  46472  caragenfiiuncl  46520  caragenunicl  46529  isomennd  46536  hoicvr  46553  ovnssle  46566  ovn0  46571  ovnsubadd  46577  hoidmvval0b  46595  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvle  46605  ovnhoilem1  46606  ovnhoi  46608  ovnlecvr2  46615  hoiqssbl  46630  hspmbllem2  46632  hspmbl  46634  vonhoire  46677  iunhoiioo  46681  vonioo  46687  vonicc  46690  vonsn  46696  smfpimltxr  46752  smfpimgtxr  46785  smfrec  46794  fmtnoprmfac1  47570  fmtnoprmfac2  47572  lighneallem3  47612  pgn4cyclex  48120