Theorem neqne 2966

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  exmidne  2968  domwdom  9537  epnsym  9579  dfac2b  10115  fin23lem14  10318  axcc2lem  10421  fiminre2  12164  cshw1  14861  xptrrel  15019  dvdsabseq  16372  ncoprmgcdne1b  16709  sgrp2rid2  18989  symg2bas  19464  symgextf  19488  odlem1  19606  gexlem1  19650  ablsimpgfind  20183  psgndiflemB  21731  cply1mul  22437  dmatmul  22635  mdetdiag  22737  mdetunilem9  22758  maducoeval2  22778  madurid  22782  chfacfisf  22992  chfacfisfcpmat  22993  plyexmo  26455  aalioulem3  26478  dvradcnv  26565  logtayllem  26805  logtayl  26806  upgriswlk  29971  lfgrwlkprop  30016  2pthnloop  30061  umgr2adedgspth  30278  umgrclwwlkge2  30323  n4cyclfrgr  30623  frgrwopreglem3  30646  frgrregorufr0  30656  domnmuln0rd  33578  elrspunsn  33718  drnglring  33763  dflringlem3  33767  dflring4  33769  satfv1lem  35835  bj-rest10b  37712  aks6d1c2p2  42867  sticksstones10  42903  sticksstones12a  42905  sticksstones12  42906  aks6d1c6lem3  42920  aks6d1c7  42932  unitscyglem2  42944  xppss12  42981  sn-0tie0  43206  prjspnfv01  43339  prjspner01  43340  fiiuncl  45768  disjf1  45884  fzisoeu  46002  fzdifsuc2  46012  supxrge  46037  suplesup  46038  infrpge  46050  xrlexaddrp  46051  infleinflem1  46068  infleinflem2  46069  infleinf  46070  xralrple3  46072  xrralrecnnge  46088  infxrpnf  46143  supminfxr  46161  fsumsupp0  46277  limcresiooub  46339  limcresioolb  46340  limclr  46352  climisp  46443  climxlim2lem  46542  dfxlim2v  46544  xlimliminflimsup  46559  icccncfext  46584  cncfiooiccre  46592  dvbdfbdioolem2  46626  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  dvnxpaek  46639  dvnprodlem3  46645  itgioocnicc  46674  ovolsplit  46685  stoweidlem14  46711  stoweidlem55  46752  stoweid  46760  dirkertrigeqlem3  46797  dirkertrigeq  46798  dirkercncf  46804  fourierdlem9  46813  fourierdlem30  46834  fourierdlem31  46835  fourierdlem33  46837  fourierdlem34  46838  fourierdlem35  46839  fourierdlem42  46846  fourierdlem43  46847  fourierdlem46  46849  fourierdlem48  46851  fourierdlem49  46852  fourierdlem51  46854  fourierdlem54  46857  fourierdlem62  46865  fourierdlem64  46867  fourierdlem65  46868  fourierdlem70  46873  fourierdlem71  46874  fourierdlem73  46876  fourierdlem74  46877  fourierdlem75  46878  fourierdlem76  46879  fourierdlem79  46882  fourierdlem81  46884  fourierdlem82  46885  fourierdlem89  46892  fourierdlem91  46894  fourierdlem102  46905  fourierdlem114  46917  sqwvfoura  46925  fourierswlem  46927  fouriersw  46928  elaa2lem  46930  etransclem25  46956  etransclem28  46959  etransclem35  46966  etransclem38  46969  qndenserrnbl  46992  ioorrnopn  47002  ioorrnopnxrlem  47003  ioorrnopnxr  47004  prsal  47015  issalnnd  47042  sge0cl  47078  sge0pr  47091  sge0prle  47098  sge0isum  47124  sge0xaddlem1  47130  iundjiun  47157  meadjun  47159  ismeannd  47164  caragenfiiuncl  47212  caragenunicl  47221  isomennd  47228  hoicvr  47245  ovnssle  47258  ovn0  47263  ovnsubadd  47269  hoidmvval0b  47287  hoidmvlelem2  47293  hoidmvlelem3  47294  hoidmvle  47297  ovnhoilem1  47298  ovnhoi  47300  ovnlecvr2  47307  hoiqssbl  47322  hspmbllem2  47324  hspmbl  47326  vonhoire  47369  iunhoiioo  47373  vonioo  47379  vonicc  47382  vonsn  47388  smfpimltxr  47444  smfpimgtxr  47477  smfrec  47486  fmtnoprmfac1  48300  fmtnoprmfac2  48302  lighneallem3  48342  pgn4cyclex  48874