Theorem neqne 2940

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

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

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 2933

This theorem is referenced by:  exmidne  2942  domwdom  9586  epnsym  9621  dfac2b  10143  fin23lem14  10345  axcc2lem  10448  fiminre2  12188  cshw1  14838  xptrrel  14997  dvdsabseq  16330  ncoprmgcdne1b  16667  sgrp2rid2  18902  symg2bas  19372  symgextf  19396  odlem1  19514  gexlem1  19558  ablsimpgfind  20091  psgndiflemB  21558  cply1mul  22232  dmatmul  22433  mdetdiag  22535  mdetunilem9  22556  maducoeval2  22576  madurid  22580  chfacfisf  22790  chfacfisfcpmat  22791  plyexmo  26271  aalioulem3  26292  dvradcnv  26380  logtayllem  26618  logtayl  26619  upgriswlk  29567  lfgrwlkprop  29613  2pthnloop  29659  umgr2adedgspth  29876  umgrclwwlkge2  29918  n4cyclfrgr  30218  frgrwopreglem3  30241  frgrregorufr0  30251  domnmuln0rd  33215  elrspunsn  33390  satfv1lem  35330  bj-rest10b  37053  aks6d1c2p2  42078  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  aks6d1c6lem3  42131  aks6d1c7  42143  unitscyglem2  42155  metakunt2  42165  xppss12  42226  sn-0tie0  42429  prjspnfv01  42594  prjspner01  42595  fiiuncl  45037  disjf1  45155  fzisoeu  45277  fzdifsuc2  45287  supxrge  45313  suplesup  45314  infrpge  45326  xrlexaddrp  45327  infleinflem1  45345  infleinflem2  45346  infleinf  45347  xralrple3  45349  xrralrecnnge  45365  infxrpnf  45421  supminfxr  45439  fsumsupp0  45555  limcresiooub  45619  limcresioolb  45620  limclr  45632  climisp  45723  climxlim2lem  45822  dfxlim2v  45824  xlimliminflimsup  45839  icccncfext  45864  cncfiooiccre  45872  dvbdfbdioolem2  45906  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnxpaek  45919  dvnprodlem3  45925  itgioocnicc  45954  ovolsplit  45965  stoweidlem14  45991  stoweidlem55  46032  stoweid  46040  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkercncf  46084  fourierdlem9  46093  fourierdlem30  46114  fourierdlem31  46115  fourierdlem33  46117  fourierdlem34  46118  fourierdlem35  46119  fourierdlem42  46126  fourierdlem43  46127  fourierdlem46  46129  fourierdlem48  46131  fourierdlem49  46132  fourierdlem51  46134  fourierdlem54  46137  fourierdlem62  46145  fourierdlem64  46147  fourierdlem65  46148  fourierdlem70  46153  fourierdlem71  46154  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem79  46162  fourierdlem81  46164  fourierdlem82  46165  fourierdlem89  46172  fourierdlem91  46174  fourierdlem102  46185  fourierdlem114  46197  sqwvfoura  46205  fourierswlem  46207  fouriersw  46208  elaa2lem  46210  etransclem25  46236  etransclem28  46239  etransclem35  46246  etransclem38  46249  qndenserrnbl  46272  ioorrnopn  46282  ioorrnopnxrlem  46283  ioorrnopnxr  46284  prsal  46295  issalnnd  46322  sge0cl  46358  sge0pr  46371  sge0prle  46378  sge0isum  46404  sge0xaddlem1  46410  iundjiun  46437  meadjun  46439  ismeannd  46444  caragenfiiuncl  46492  caragenunicl  46501  isomennd  46508  hoicvr  46525  ovnssle  46538  ovn0  46543  ovnsubadd  46549  hoidmvval0b  46567  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvle  46577  ovnhoilem1  46578  ovnhoi  46580  ovnlecvr2  46587  hoiqssbl  46602  hspmbllem2  46604  hspmbl  46606  vonhoire  46649  iunhoiioo  46653  vonioo  46659  vonicc  46662  vonsn  46668  smfpimltxr  46724  smfpimgtxr  46757  smfrec  46766  fmtnoprmfac1  47527  fmtnoprmfac2  47529  lighneallem3  47569