Theorem neqne 2947

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

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

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 206  df-ne 2940

This theorem is referenced by:  exmidne  2949  2f1fvneq  7262  domwdom  9575  epnsym  9610  dfac2b  10131  fin23lem14  10334  axcc2lem  10437  fiminre2  12169  cshw1  14779  xptrrel  14934  dvdsabseq  16263  ncoprmgcdne1b  16594  sgrp2rid2  18849  symg2bas  19308  symgextf  19333  odlem1  19451  gexlem1  19495  ablsimpgfind  20028  psgndiflemB  21463  cply1mul  22138  dmatmul  22319  mdetdiag  22421  mdetunilem9  22442  maducoeval2  22462  madurid  22466  chfacfisf  22676  chfacfisfcpmat  22677  plyexmo  26165  aalioulem3  26186  dvradcnv  26272  logtayllem  26507  logtayl  26508  upgriswlk  29332  lfgrwlkprop  29378  2pthnloop  29422  umgr2adedgspth  29636  umgrclwwlkge2  29678  n4cyclfrgr  29978  frgrwopreglem3  30001  frgrregorufr0  30011  elrspunsn  32988  satfv1lem  34818  bj-rest10b  36436  aks6d1c2p2  41426  sticksstones10  41440  sticksstones12a  41442  sticksstones12  41443  metakunt2  41455  xppss12  41516  sn-0tie0  41777  prjspnfv01  41831  prjspner01  41832  fiiuncl  44216  disjf1  44343  fzisoeu  44471  fzdifsuc2  44481  supxrge  44509  suplesup  44510  infrpge  44522  xrlexaddrp  44523  infleinflem1  44541  infleinflem2  44542  infleinf  44543  xralrple3  44545  xrralrecnnge  44561  infxrpnf  44617  supminfxr  44635  fsumsupp0  44755  limcresiooub  44819  limcresioolb  44820  limclr  44832  climisp  44923  climxlim2lem  45022  dfxlim2v  45024  xlimliminflimsup  45039  icccncfext  45064  cncfiooiccre  45072  dvbdfbdioolem2  45106  ioodvbdlimc1lem2  45109  ioodvbdlimc2lem  45111  dvnxpaek  45119  dvnprodlem3  45125  itgioocnicc  45154  ovolsplit  45165  stoweidlem14  45191  stoweidlem55  45232  stoweid  45240  dirkertrigeqlem3  45277  dirkertrigeq  45278  dirkercncf  45284  fourierdlem9  45293  fourierdlem30  45314  fourierdlem31  45315  fourierdlem33  45317  fourierdlem34  45318  fourierdlem35  45319  fourierdlem42  45326  fourierdlem43  45327  fourierdlem46  45329  fourierdlem48  45331  fourierdlem49  45332  fourierdlem51  45334  fourierdlem54  45337  fourierdlem62  45345  fourierdlem64  45347  fourierdlem65  45348  fourierdlem70  45353  fourierdlem71  45354  fourierdlem73  45356  fourierdlem74  45357  fourierdlem75  45358  fourierdlem76  45359  fourierdlem79  45362  fourierdlem81  45364  fourierdlem82  45365  fourierdlem89  45372  fourierdlem91  45374  fourierdlem102  45385  fourierdlem114  45397  sqwvfoura  45405  fourierswlem  45407  fouriersw  45408  elaa2lem  45410  etransclem25  45436  etransclem28  45439  etransclem35  45446  etransclem38  45449  qndenserrnbl  45472  ioorrnopn  45482  ioorrnopnxrlem  45483  ioorrnopnxr  45484  prsal  45495  issalnnd  45522  sge0cl  45558  sge0pr  45571  sge0prle  45578  sge0isum  45604  sge0xaddlem1  45610  iundjiun  45637  meadjun  45639  ismeannd  45644  caragenfiiuncl  45692  caragenunicl  45701  isomennd  45708  hoicvr  45725  ovnssle  45738  ovn0  45743  ovnsubadd  45749  hoidmvval0b  45767  hoidmvlelem2  45773  hoidmvlelem3  45774  hoidmvle  45777  ovnhoilem1  45778  ovnhoi  45780  ovnlecvr2  45787  hoiqssbl  45802  hspmbllem2  45804  hspmbl  45806  vonhoire  45849  iunhoiioo  45853  vonioo  45859  vonicc  45862  vonsn  45868  smfpimltxr  45924  smfpimgtxr  45957  smfrec  45966  fmtnoprmfac1  46694  fmtnoprmfac2  46696  lighneallem3  46736