Theorem neqne 2941

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  exmidne  2943  domwdom  9491  epnsym  9530  dfac2b  10053  fin23lem14  10255  axcc2lem  10358  fiminre2  12102  cshw1  14757  xptrrel  14915  dvdsabseq  16252  ncoprmgcdne1b  16589  sgrp2rid2  18863  symg2bas  19334  symgextf  19358  odlem1  19476  gexlem1  19520  ablsimpgfind  20053  psgndiflemB  21567  cply1mul  22252  dmatmul  22453  mdetdiag  22555  mdetunilem9  22576  maducoeval2  22596  madurid  22600  chfacfisf  22810  chfacfisfcpmat  22811  plyexmo  26289  aalioulem3  26310  dvradcnv  26398  logtayllem  26636  logtayl  26637  upgriswlk  29726  lfgrwlkprop  29771  2pthnloop  29816  umgr2adedgspth  30033  umgrclwwlkge2  30078  n4cyclfrgr  30378  frgrwopreglem3  30401  frgrregorufr0  30411  domnmuln0rd  33367  elrspunsn  33521  satfv1lem  35575  bj-rest10b  37339  aks6d1c2p2  42486  sticksstones10  42522  sticksstones12a  42524  sticksstones12  42525  aks6d1c6lem3  42539  aks6d1c7  42551  unitscyglem2  42563  xppss12  42598  sn-0tie0  42818  prjspnfv01  42979  prjspner01  42980  fiiuncl  45422  disjf1  45539  fzisoeu  45659  fzdifsuc2  45669  supxrge  45694  suplesup  45695  infrpge  45707  xrlexaddrp  45708  infleinflem1  45725  infleinflem2  45726  infleinf  45727  xralrple3  45729  xrralrecnnge  45745  infxrpnf  45801  supminfxr  45819  fsumsupp0  45935  limcresiooub  45997  limcresioolb  45998  limclr  46010  climisp  46101  climxlim2lem  46200  dfxlim2v  46202  xlimliminflimsup  46217  icccncfext  46242  cncfiooiccre  46250  dvbdfbdioolem2  46284  ioodvbdlimc1lem2  46287  ioodvbdlimc2lem  46289  dvnxpaek  46297  dvnprodlem3  46303  itgioocnicc  46332  ovolsplit  46343  stoweidlem14  46369  stoweidlem55  46410  stoweid  46418  dirkertrigeqlem3  46455  dirkertrigeq  46456  dirkercncf  46462  fourierdlem9  46471  fourierdlem30  46492  fourierdlem31  46493  fourierdlem33  46495  fourierdlem34  46496  fourierdlem35  46497  fourierdlem42  46504  fourierdlem43  46505  fourierdlem46  46507  fourierdlem48  46509  fourierdlem49  46510  fourierdlem51  46512  fourierdlem54  46515  fourierdlem62  46523  fourierdlem64  46525  fourierdlem65  46526  fourierdlem70  46531  fourierdlem71  46532  fourierdlem73  46534  fourierdlem74  46535  fourierdlem75  46536  fourierdlem76  46537  fourierdlem79  46540  fourierdlem81  46542  fourierdlem82  46543  fourierdlem89  46550  fourierdlem91  46552  fourierdlem102  46563  fourierdlem114  46575  sqwvfoura  46583  fourierswlem  46585  fouriersw  46586  elaa2lem  46588  etransclem25  46614  etransclem28  46617  etransclem35  46624  etransclem38  46627  qndenserrnbl  46650  ioorrnopn  46660  ioorrnopnxrlem  46661  ioorrnopnxr  46662  prsal  46673  issalnnd  46700  sge0cl  46736  sge0pr  46749  sge0prle  46756  sge0isum  46782  sge0xaddlem1  46788  iundjiun  46815  meadjun  46817  ismeannd  46822  caragenfiiuncl  46870  caragenunicl  46879  isomennd  46886  hoicvr  46903  ovnssle  46916  ovn0  46921  ovnsubadd  46927  hoidmvval0b  46945  hoidmvlelem2  46951  hoidmvlelem3  46952  hoidmvle  46955  ovnhoilem1  46956  ovnhoi  46958  ovnlecvr2  46965  hoiqssbl  46980  hspmbllem2  46982  hspmbl  46984  vonhoire  47027  iunhoiioo  47031  vonioo  47037  vonicc  47040  vonsn  47046  smfpimltxr  47102  smfpimgtxr  47135  smfrec  47144  fmtnoprmfac1  47922  fmtnoprmfac2  47924  lighneallem3  47964  pgn4cyclex  48483