Theorem neqne 2933

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

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

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 2926

This theorem is referenced by:  exmidne  2935  domwdom  9527  epnsym  9562  dfac2b  10084  fin23lem14  10286  axcc2lem  10389  fiminre2  12131  cshw1  14787  xptrrel  14946  dvdsabseq  16283  ncoprmgcdne1b  16620  sgrp2rid2  18853  symg2bas  19323  symgextf  19347  odlem1  19465  gexlem1  19509  ablsimpgfind  20042  psgndiflemB  21509  cply1mul  22183  dmatmul  22384  mdetdiag  22486  mdetunilem9  22507  maducoeval2  22527  madurid  22531  chfacfisf  22741  chfacfisfcpmat  22742  plyexmo  26221  aalioulem3  26242  dvradcnv  26330  logtayllem  26568  logtayl  26569  upgriswlk  29569  lfgrwlkprop  29615  2pthnloop  29661  umgr2adedgspth  29878  umgrclwwlkge2  29920  n4cyclfrgr  30220  frgrwopreglem3  30243  frgrregorufr0  30253  domnmuln0rd  33225  elrspunsn  33400  satfv1lem  35349  bj-rest10b  37077  aks6d1c2p2  42107  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  aks6d1c6lem3  42160  aks6d1c7  42172  unitscyglem2  42184  xppss12  42217  sn-0tie0  42439  prjspnfv01  42612  prjspner01  42613  fiiuncl  45059  disjf1  45177  fzisoeu  45298  fzdifsuc2  45308  supxrge  45334  suplesup  45335  infrpge  45347  xrlexaddrp  45348  infleinflem1  45366  infleinflem2  45367  infleinf  45368  xralrple3  45370  xrralrecnnge  45386  infxrpnf  45442  supminfxr  45460  fsumsupp0  45576  limcresiooub  45640  limcresioolb  45641  limclr  45653  climisp  45744  climxlim2lem  45843  dfxlim2v  45845  xlimliminflimsup  45860  icccncfext  45885  cncfiooiccre  45893  dvbdfbdioolem2  45927  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnxpaek  45940  dvnprodlem3  45946  itgioocnicc  45975  ovolsplit  45986  stoweidlem14  46012  stoweidlem55  46053  stoweid  46061  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkercncf  46105  fourierdlem9  46114  fourierdlem30  46135  fourierdlem31  46136  fourierdlem33  46138  fourierdlem34  46139  fourierdlem35  46140  fourierdlem42  46147  fourierdlem43  46148  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem51  46155  fourierdlem54  46158  fourierdlem62  46166  fourierdlem64  46168  fourierdlem65  46169  fourierdlem70  46174  fourierdlem71  46175  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem79  46183  fourierdlem81  46185  fourierdlem82  46186  fourierdlem89  46193  fourierdlem91  46195  fourierdlem102  46206  fourierdlem114  46218  sqwvfoura  46226  fourierswlem  46228  fouriersw  46229  elaa2lem  46231  etransclem25  46257  etransclem28  46260  etransclem35  46267  etransclem38  46270  qndenserrnbl  46293  ioorrnopn  46303  ioorrnopnxrlem  46304  ioorrnopnxr  46305  prsal  46316  issalnnd  46343  sge0cl  46379  sge0pr  46392  sge0prle  46399  sge0isum  46425  sge0xaddlem1  46431  iundjiun  46458  meadjun  46460  ismeannd  46465  caragenfiiuncl  46513  caragenunicl  46522  isomennd  46529  hoicvr  46546  ovnssle  46559  ovn0  46564  ovnsubadd  46570  hoidmvval0b  46588  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvle  46598  ovnhoilem1  46599  ovnhoi  46601  ovnlecvr2  46608  hoiqssbl  46623  hspmbllem2  46625  hspmbl  46627  vonhoire  46670  iunhoiioo  46674  vonioo  46680  vonicc  46683  vonsn  46689  smfpimltxr  46745  smfpimgtxr  46778  smfrec  46787  fmtnoprmfac1  47566  fmtnoprmfac2  47568  lighneallem3  47608  pgn4cyclex  48116