Theorem neqne 2963

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 23	. 2 ⊢ (¬ 𝐴 = 𝐵 → ¬ 𝐴 = 𝐵)
2	1	neqned 2962	1 ⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  exmidne  2965  domwdom  9546  epnsym  9588  dfac2b  10133  fin23lem14  10335  axcc2lem  10438  fiminre2  12187  cshw1  14893  xptrrel  15053  dvdsabseq  16403  ncoprmgcdne1b  16740  sgrp2rid2  19038  symg2bas  19520  symgextf  19544  odlem1  19662  gexlem1  19706  ablsimpgfind  20239  psgndiflemB  21813  cply1mul  22521  dmatmul  22719  mdetdiag  22821  mdetunilem9  22842  maducoeval2  22862  madurid  22866  chfacfisf  23079  chfacfisfcpmat  23080  plyexmo  26545  aalioulem3  26570  dvradcnv  26657  logtayllem  26896  logtayl  26897  upgriswlk  30100  lfgrwlkprop  30149  2pthnloop  30196  umgr2adedgspth  30416  umgrclwwlkge2  30461  n4cyclfrgr  30771  frgrwopreglem3  30794  frgrregorufr0  30804  domnmuln0rd  33717  elrspunsn  33857  drnglring  33902  dflringlem3  33906  dflring4  33908  satfv1lem  35941  bj-rest10b  37839  aks6d1c2p2  42985  sticksstones10  43021  sticksstones12a  43023  sticksstones12  43024  aks6d1c6lem3  43038  aks6d1c7  43050  unitscyglem2  43062  xppss12  43099  sn-0tie0  43339  prjspnfv01  43470  prjspner01  43471  fiiuncl  45899  disjf1  46015  fzisoeu  46133  fzdifsuc2  46143  supxrge  46168  suplesup  46169  infrpge  46181  xrlexaddrp  46182  infleinflem1  46199  infleinflem2  46200  infleinf  46201  xralrple3  46203  xrralrecnnge  46219  infxrpnf  46274  supminfxr  46292  fsumsupp0  46408  limcresiooub  46470  limcresioolb  46471  limclr  46483  climisp  46574  climxlim2lem  46673  dfxlim2v  46675  xlimliminflimsup  46690  icccncfext  46715  cncfiooiccre  46723  dvbdfbdioolem2  46757  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  dvnxpaek  46770  dvnprodlem3  46776  itgioocnicc  46805  ovolsplit  46816  stoweidlem14  46842  stoweidlem55  46883  stoweid  46891  dirkertrigeqlem3  46928  dirkertrigeq  46929  dirkercncf  46935  fourierdlem9  46944  fourierdlem30  46965  fourierdlem31  46966  fourierdlem33  46968  fourierdlem34  46969  fourierdlem35  46970  fourierdlem42  46977  fourierdlem43  46978  fourierdlem46  46980  fourierdlem48  46982  fourierdlem49  46983  fourierdlem51  46985  fourierdlem54  46988  fourierdlem62  46996  fourierdlem64  46998  fourierdlem65  46999  fourierdlem70  47004  fourierdlem71  47005  fourierdlem73  47007  fourierdlem74  47008  fourierdlem75  47009  fourierdlem76  47010  fourierdlem79  47013  fourierdlem81  47015  fourierdlem82  47016  fourierdlem89  47023  fourierdlem91  47025  fourierdlem102  47036  fourierdlem114  47048  sqwvfoura  47056  fourierswlem  47058  fouriersw  47059  elaa2lem  47061  etransclem25  47087  etransclem28  47090  etransclem35  47097  etransclem38  47100  qndenserrnbl  47123  ioorrnopn  47133  ioorrnopnxrlem  47134  ioorrnopnxr  47135  prsal  47146  issalnnd  47173  sge0cl  47209  sge0pr  47222  sge0prle  47229  sge0isum  47255  sge0xaddlem1  47261  iundjiun  47288  meadjun  47290  ismeannd  47295  caragenfiiuncl  47343  caragenunicl  47352  isomennd  47359  hoicvr  47376  ovnssle  47389  ovn0  47394  ovnsubadd  47400  hoidmvval0b  47418  hoidmvlelem2  47424  hoidmvlelem3  47425  hoidmvle  47428  ovnhoilem1  47429  ovnhoi  47431  ovnlecvr2  47438  hoiqssbl  47453  hspmbllem2  47455  hspmbl  47457  vonhoire  47500  iunhoiioo  47504  vonioo  47510  vonicc  47513  vonsn  47519  smfpimltxr  47575  smfpimgtxr  47608  smfrec  47617  fmtnoprmfac1  48468  fmtnoprmfac2  48470  lighneallem3  48510  pgn4cyclex  49042