Theorem neqne 3024

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3016

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 209  df-ne 3017

This theorem is referenced by:  exmidne  3026  2f1fvneq  7018  domwdom  9038  epnsym  9072  dfac2b  9556  fin23lem14  9755  axcc2lem  9858  cshw1  14184  xptrrel  14340  pwm1geoserOLD  15225  dvdsabseq  15663  ncoprmgcdne1b  15994  sgrp2rid2  18091  symg2bas  18521  symgextf  18545  odlem1  18663  gexlem1  18704  ablsimpgfind  19232  cply1mul  20462  psgndiflemB  20744  dmatmul  21106  mdetdiag  21208  mdetunilem9  21229  maducoeval2  21249  madurid  21253  chfacfisf  21462  chfacfisfcpmat  21463  plyexmo  24902  aalioulem3  24923  dvradcnv  25009  logtayllem  25242  logtayl  25243  upgriswlk  27422  lfgrwlkprop  27469  2pthnloop  27512  umgr2adedgspth  27727  umgrclwwlkge2  27769  n4cyclfrgr  28070  frgrwopreglem3  28093  frgrregorufr0  28103  satfv1lem  32609  bj-rest10b  34383  xppss12  39164  fiiuncl  41376  disjf1  41492  fzisoeu  41616  fzdifsuc2  41626  supxrge  41655  suplesup  41656  infrpge  41668  xrlexaddrp  41669  infleinflem1  41687  infleinflem2  41688  infleinf  41689  xralrple3  41691  fiminre2  41695  xrralrecnnge  41711  infxrpnf  41770  supminfxr  41789  fsumsupp0  41908  limcresiooub  41972  limcresioolb  41973  limclr  41985  climisp  42076  climxlim2lem  42175  dfxlim2v  42177  xlimliminflimsup  42192  icccncfext  42219  cncfiooiccre  42227  dvbdfbdioolem2  42263  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnxpaek  42276  dvnprodlem3  42282  itgioocnicc  42311  ovolsplit  42322  stoweidlem14  42348  stoweidlem55  42389  stoweid  42397  dirkertrigeqlem3  42434  dirkertrigeq  42435  dirkercncf  42441  fourierdlem9  42450  fourierdlem30  42471  fourierdlem31  42472  fourierdlem33  42474  fourierdlem34  42475  fourierdlem35  42476  fourierdlem42  42483  fourierdlem43  42484  fourierdlem46  42486  fourierdlem48  42488  fourierdlem49  42489  fourierdlem51  42491  fourierdlem54  42494  fourierdlem62  42502  fourierdlem64  42504  fourierdlem65  42505  fourierdlem70  42510  fourierdlem71  42511  fourierdlem73  42513  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem79  42519  fourierdlem81  42521  fourierdlem82  42522  fourierdlem89  42529  fourierdlem91  42531  fourierdlem102  42542  fourierdlem114  42554  sqwvfoura  42562  fourierswlem  42564  fouriersw  42565  elaa2lem  42567  etransclem25  42593  etransclem28  42596  etransclem35  42603  etransclem38  42606  qndenserrnbl  42629  ioorrnopn  42639  ioorrnopnxrlem  42640  ioorrnopnxr  42641  prsal  42652  issalnnd  42677  sge0cl  42712  sge0pr  42725  sge0prle  42732  sge0isum  42758  sge0xaddlem1  42764  iundjiun  42791  meadjun  42793  ismeannd  42798  caragenfiiuncl  42846  caragenunicl  42855  isomennd  42862  hoicvr  42879  ovnssle  42892  ovn0  42897  ovnsubadd  42903  hoidmvval0b  42921  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvle  42931  ovnhoilem1  42932  ovnhoi  42934  ovnlecvr2  42941  hoiqssbl  42956  hspmbllem2  42958  hspmbl  42960  vonhoire  43003  iunhoiioo  43007  vonioo  43013  vonicc  43016  vonsn  43022  smfpimltxr  43073  smfpimgtxr  43105  smfrec  43113  fmtnoprmfac1  43776  fmtnoprmfac2  43778  lighneallem3  43821