Theorem neqne 2964

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 2957

This theorem is referenced by:  exmidne  2966  domwdom  9516  epnsym  9558  dfac2b  10081  fin23lem14  10284  axcc2lem  10387  fiminre2  12134  cshw1  14829  xptrrel  14987  dvdsabseq  16338  ncoprmgcdne1b  16675  sgrp2rid2  18954  symg2bas  19424  symgextf  19448  odlem1  19566  gexlem1  19610  ablsimpgfind  20143  psgndiflemB  21640  cply1mul  22347  dmatmul  22545  mdetdiag  22647  mdetunilem9  22668  maducoeval2  22688  madurid  22692  chfacfisf  22902  chfacfisfcpmat  22903  plyexmo  26365  aalioulem3  26386  dvradcnv  26472  logtayllem  26712  logtayl  26713  upgriswlk  29798  lfgrwlkprop  29843  2pthnloop  29888  umgr2adedgspth  30105  umgrclwwlkge2  30150  n4cyclfrgr  30450  frgrwopreglem3  30473  frgrregorufr0  30483  domnmuln0rd  33419  elrspunsn  33576  drnglring  33649  dflringlem3  33653  dflring4  33655  satfv1lem  35673  bj-rest10b  37540  aks6d1c2p2  42697  sticksstones10  42733  sticksstones12a  42735  sticksstones12  42736  aks6d1c6lem3  42750  aks6d1c7  42762  unitscyglem2  42774  xppss12  42809  sn-0tie0  43034  prjspnfv01  43167  prjspner01  43168  fiiuncl  45606  disjf1  45722  fzisoeu  45840  fzdifsuc2  45850  supxrge  45875  suplesup  45876  infrpge  45888  xrlexaddrp  45889  infleinflem1  45906  infleinflem2  45907  infleinf  45908  xralrple3  45910  xrralrecnnge  45926  infxrpnf  45981  supminfxr  45999  fsumsupp0  46115  limcresiooub  46177  limcresioolb  46178  limclr  46190  climisp  46281  climxlim2lem  46380  dfxlim2v  46382  xlimliminflimsup  46397  icccncfext  46422  cncfiooiccre  46430  dvbdfbdioolem2  46464  ioodvbdlimc1lem2  46467  ioodvbdlimc2lem  46469  dvnxpaek  46477  dvnprodlem3  46483  itgioocnicc  46512  ovolsplit  46523  stoweidlem14  46549  stoweidlem55  46590  stoweid  46598  dirkertrigeqlem3  46635  dirkertrigeq  46636  dirkercncf  46642  fourierdlem9  46651  fourierdlem30  46672  fourierdlem31  46673  fourierdlem33  46675  fourierdlem34  46676  fourierdlem35  46677  fourierdlem42  46684  fourierdlem43  46685  fourierdlem46  46687  fourierdlem48  46689  fourierdlem49  46690  fourierdlem51  46692  fourierdlem54  46695  fourierdlem62  46703  fourierdlem64  46705  fourierdlem65  46706  fourierdlem70  46711  fourierdlem71  46712  fourierdlem73  46714  fourierdlem74  46715  fourierdlem75  46716  fourierdlem76  46717  fourierdlem79  46720  fourierdlem81  46722  fourierdlem82  46723  fourierdlem89  46730  fourierdlem91  46732  fourierdlem102  46743  fourierdlem114  46755  sqwvfoura  46763  fourierswlem  46765  fouriersw  46766  elaa2lem  46768  etransclem25  46794  etransclem28  46797  etransclem35  46804  etransclem38  46807  qndenserrnbl  46830  ioorrnopn  46840  ioorrnopnxrlem  46841  ioorrnopnxr  46842  prsal  46853  issalnnd  46880  sge0cl  46916  sge0pr  46929  sge0prle  46936  sge0isum  46962  sge0xaddlem1  46968  iundjiun  46995  meadjun  46997  ismeannd  47002  caragenfiiuncl  47050  caragenunicl  47059  isomennd  47066  hoicvr  47083  ovnssle  47096  ovn0  47101  ovnsubadd  47107  hoidmvval0b  47125  hoidmvlelem2  47131  hoidmvlelem3  47132  hoidmvle  47135  ovnhoilem1  47136  ovnhoi  47138  ovnlecvr2  47145  hoiqssbl  47160  hspmbllem2  47162  hspmbl  47164  vonhoire  47207  iunhoiioo  47211  vonioo  47217  vonicc  47220  vonsn  47226  smfpimltxr  47282  smfpimgtxr  47315  smfrec  47324  fmtnoprmfac1  48135  fmtnoprmfac2  48137  lighneallem3  48177  pgn4cyclex  48709