Theorem neqne 2951

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

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

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 2944

This theorem is referenced by:  exmidne  2953  2f1fvneq  7133  domwdom  9333  epnsym  9367  dfac2b  9886  fin23lem14  10089  axcc2lem  10192  fiminre2  11923  cshw1  14535  xptrrel  14691  dvdsabseq  16022  ncoprmgcdne1b  16355  sgrp2rid2  18565  symg2bas  19000  symgextf  19025  odlem1  19143  gexlem1  19184  ablsimpgfind  19713  psgndiflemB  20805  cply1mul  21465  dmatmul  21646  mdetdiag  21748  mdetunilem9  21769  maducoeval2  21789  madurid  21793  chfacfisf  22003  chfacfisfcpmat  22004  plyexmo  25473  aalioulem3  25494  dvradcnv  25580  logtayllem  25814  logtayl  25815  upgriswlk  28008  lfgrwlkprop  28055  2pthnloop  28099  umgr2adedgspth  28313  umgrclwwlkge2  28355  n4cyclfrgr  28655  frgrwopreglem3  28678  frgrregorufr0  28688  satfv1lem  33324  bj-rest10b  35260  sticksstones10  40111  sticksstones12a  40113  sticksstones12  40114  metakunt2  40126  xppss12  40204  sn-0tie0  40421  prjspnfv01  40461  prjspner01  40462  fiiuncl  42613  disjf1  42720  fzisoeu  42839  fzdifsuc2  42849  supxrge  42877  suplesup  42878  infrpge  42890  xrlexaddrp  42891  infleinflem1  42909  infleinflem2  42910  infleinf  42911  xralrple3  42913  xrralrecnnge  42930  infxrpnf  42986  supminfxr  43004  fsumsupp0  43119  limcresiooub  43183  limcresioolb  43184  limclr  43196  climisp  43287  climxlim2lem  43386  dfxlim2v  43388  xlimliminflimsup  43403  icccncfext  43428  cncfiooiccre  43436  dvbdfbdioolem2  43470  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  dvnxpaek  43483  dvnprodlem3  43489  itgioocnicc  43518  ovolsplit  43529  stoweidlem14  43555  stoweidlem55  43596  stoweid  43604  dirkertrigeqlem3  43641  dirkertrigeq  43642  dirkercncf  43648  fourierdlem9  43657  fourierdlem30  43678  fourierdlem31  43679  fourierdlem33  43681  fourierdlem34  43682  fourierdlem35  43683  fourierdlem42  43690  fourierdlem43  43691  fourierdlem46  43693  fourierdlem48  43695  fourierdlem49  43696  fourierdlem51  43698  fourierdlem54  43701  fourierdlem62  43709  fourierdlem64  43711  fourierdlem65  43712  fourierdlem70  43717  fourierdlem71  43718  fourierdlem73  43720  fourierdlem74  43721  fourierdlem75  43722  fourierdlem76  43723  fourierdlem79  43726  fourierdlem81  43728  fourierdlem82  43729  fourierdlem89  43736  fourierdlem91  43738  fourierdlem102  43749  fourierdlem114  43761  sqwvfoura  43769  fourierswlem  43771  fouriersw  43772  elaa2lem  43774  etransclem25  43800  etransclem28  43803  etransclem35  43810  etransclem38  43813  qndenserrnbl  43836  ioorrnopn  43846  ioorrnopnxrlem  43847  ioorrnopnxr  43848  prsal  43859  issalnnd  43884  sge0cl  43919  sge0pr  43932  sge0prle  43939  sge0isum  43965  sge0xaddlem1  43971  iundjiun  43998  meadjun  44000  ismeannd  44005  caragenfiiuncl  44053  caragenunicl  44062  isomennd  44069  hoicvr  44086  ovnssle  44099  ovn0  44104  ovnsubadd  44110  hoidmvval0b  44128  hoidmvlelem2  44134  hoidmvlelem3  44135  hoidmvle  44138  ovnhoilem1  44139  ovnhoi  44141  ovnlecvr2  44148  hoiqssbl  44163  hspmbllem2  44165  hspmbl  44167  vonhoire  44210  iunhoiioo  44214  vonioo  44220  vonicc  44223  vonsn  44229  smfpimltxr  44283  smfpimgtxr  44315  smfrec  44323  fmtnoprmfac1  45017  fmtnoprmfac2  45019  lighneallem3  45059