Theorem neqne 2950

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942

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 2943

This theorem is referenced by:  exmidne  2952  2f1fvneq  7114  domwdom  9263  epnsym  9297  dfac2b  9817  fin23lem14  10020  axcc2lem  10123  fiminre2  11853  cshw1  14463  xptrrel  14619  dvdsabseq  15950  ncoprmgcdne1b  16283  sgrp2rid2  18480  symg2bas  18915  symgextf  18940  odlem1  19058  gexlem1  19099  ablsimpgfind  19628  psgndiflemB  20717  cply1mul  21375  dmatmul  21554  mdetdiag  21656  mdetunilem9  21677  maducoeval2  21697  madurid  21701  chfacfisf  21911  chfacfisfcpmat  21912  plyexmo  25378  aalioulem3  25399  dvradcnv  25485  logtayllem  25719  logtayl  25720  upgriswlk  27910  lfgrwlkprop  27957  2pthnloop  28000  umgr2adedgspth  28214  umgrclwwlkge2  28256  n4cyclfrgr  28556  frgrwopreglem3  28579  frgrregorufr0  28589  satfv1lem  33224  bj-rest10b  35187  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  metakunt2  40054  xppss12  40130  sn-0tie0  40342  prjspnfv01  40382  prjspner01  40383  fiiuncl  42502  disjf1  42609  fzisoeu  42729  fzdifsuc2  42739  supxrge  42767  suplesup  42768  infrpge  42780  xrlexaddrp  42781  infleinflem1  42799  infleinflem2  42800  infleinf  42801  xralrple3  42803  xrralrecnnge  42820  infxrpnf  42876  supminfxr  42894  fsumsupp0  43009  limcresiooub  43073  limcresioolb  43074  limclr  43086  climisp  43177  climxlim2lem  43276  dfxlim2v  43278  xlimliminflimsup  43293  icccncfext  43318  cncfiooiccre  43326  dvbdfbdioolem2  43360  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnxpaek  43373  dvnprodlem3  43379  itgioocnicc  43408  ovolsplit  43419  stoweidlem14  43445  stoweidlem55  43486  stoweid  43494  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkercncf  43538  fourierdlem9  43547  fourierdlem30  43568  fourierdlem31  43569  fourierdlem33  43571  fourierdlem34  43572  fourierdlem35  43573  fourierdlem42  43580  fourierdlem43  43581  fourierdlem46  43583  fourierdlem48  43585  fourierdlem49  43586  fourierdlem51  43588  fourierdlem54  43591  fourierdlem62  43599  fourierdlem64  43601  fourierdlem65  43602  fourierdlem70  43607  fourierdlem71  43608  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem79  43616  fourierdlem81  43618  fourierdlem82  43619  fourierdlem89  43626  fourierdlem91  43628  fourierdlem102  43639  fourierdlem114  43651  sqwvfoura  43659  fourierswlem  43661  fouriersw  43662  elaa2lem  43664  etransclem25  43690  etransclem28  43693  etransclem35  43700  etransclem38  43703  qndenserrnbl  43726  ioorrnopn  43736  ioorrnopnxrlem  43737  ioorrnopnxr  43738  prsal  43749  issalnnd  43774  sge0cl  43809  sge0pr  43822  sge0prle  43829  sge0isum  43855  sge0xaddlem1  43861  iundjiun  43888  meadjun  43890  ismeannd  43895  caragenfiiuncl  43943  caragenunicl  43952  isomennd  43959  hoicvr  43976  ovnssle  43989  ovn0  43994  ovnsubadd  44000  hoidmvval0b  44018  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvle  44028  ovnhoilem1  44029  ovnhoi  44031  ovnlecvr2  44038  hoiqssbl  44053  hspmbllem2  44055  hspmbl  44057  vonhoire  44100  iunhoiioo  44104  vonioo  44110  vonicc  44113  vonsn  44119  smfpimltxr  44170  smfpimgtxr  44202  smfrec  44210  fmtnoprmfac1  44905  fmtnoprmfac2  44907  lighneallem3  44947