Theorem neqne 2937

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2929

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 207  df-ne 2930

This theorem is referenced by:  exmidne  2939  domwdom  9471  epnsym  9510  dfac2b  10033  fin23lem14  10235  axcc2lem  10338  fiminre2  12081  cshw1  14736  xptrrel  14894  dvdsabseq  16231  ncoprmgcdne1b  16568  sgrp2rid2  18842  symg2bas  19313  symgextf  19337  odlem1  19455  gexlem1  19499  ablsimpgfind  20032  psgndiflemB  21546  cply1mul  22231  dmatmul  22432  mdetdiag  22534  mdetunilem9  22555  maducoeval2  22575  madurid  22579  chfacfisf  22789  chfacfisfcpmat  22790  plyexmo  26268  aalioulem3  26289  dvradcnv  26377  logtayllem  26615  logtayl  26616  upgriswlk  29640  lfgrwlkprop  29685  2pthnloop  29730  umgr2adedgspth  29947  umgrclwwlkge2  29992  n4cyclfrgr  30292  frgrwopreglem3  30315  frgrregorufr0  30325  domnmuln0rd  33284  elrspunsn  33438  satfv1lem  35478  bj-rest10b  37206  aks6d1c2p2  42285  sticksstones10  42321  sticksstones12a  42323  sticksstones12  42324  aks6d1c6lem3  42338  aks6d1c7  42350  unitscyglem2  42362  xppss12  42400  sn-0tie0  42621  prjspnfv01  42782  prjspner01  42783  fiiuncl  45226  disjf1  45343  fzisoeu  45464  fzdifsuc2  45474  supxrge  45499  suplesup  45500  infrpge  45512  xrlexaddrp  45513  infleinflem1  45530  infleinflem2  45531  infleinf  45532  xralrple3  45534  xrralrecnnge  45550  infxrpnf  45606  supminfxr  45624  fsumsupp0  45740  limcresiooub  45802  limcresioolb  45803  limclr  45815  climisp  45906  climxlim2lem  46005  dfxlim2v  46007  xlimliminflimsup  46022  icccncfext  46047  cncfiooiccre  46055  dvbdfbdioolem2  46089  ioodvbdlimc1lem2  46092  ioodvbdlimc2lem  46094  dvnxpaek  46102  dvnprodlem3  46108  itgioocnicc  46137  ovolsplit  46148  stoweidlem14  46174  stoweidlem55  46215  stoweid  46223  dirkertrigeqlem3  46260  dirkertrigeq  46261  dirkercncf  46267  fourierdlem9  46276  fourierdlem30  46297  fourierdlem31  46298  fourierdlem33  46300  fourierdlem34  46301  fourierdlem35  46302  fourierdlem42  46309  fourierdlem43  46310  fourierdlem46  46312  fourierdlem48  46314  fourierdlem49  46315  fourierdlem51  46317  fourierdlem54  46320  fourierdlem62  46328  fourierdlem64  46330  fourierdlem65  46331  fourierdlem70  46336  fourierdlem71  46337  fourierdlem73  46339  fourierdlem74  46340  fourierdlem75  46341  fourierdlem76  46342  fourierdlem79  46345  fourierdlem81  46347  fourierdlem82  46348  fourierdlem89  46355  fourierdlem91  46357  fourierdlem102  46368  fourierdlem114  46380  sqwvfoura  46388  fourierswlem  46390  fouriersw  46391  elaa2lem  46393  etransclem25  46419  etransclem28  46422  etransclem35  46429  etransclem38  46432  qndenserrnbl  46455  ioorrnopn  46465  ioorrnopnxrlem  46466  ioorrnopnxr  46467  prsal  46478  issalnnd  46505  sge0cl  46541  sge0pr  46554  sge0prle  46561  sge0isum  46587  sge0xaddlem1  46593  iundjiun  46620  meadjun  46622  ismeannd  46627  caragenfiiuncl  46675  caragenunicl  46684  isomennd  46691  hoicvr  46708  ovnssle  46721  ovn0  46726  ovnsubadd  46732  hoidmvval0b  46750  hoidmvlelem2  46756  hoidmvlelem3  46757  hoidmvle  46760  ovnhoilem1  46761  ovnhoi  46763  ovnlecvr2  46770  hoiqssbl  46785  hspmbllem2  46787  hspmbl  46789  vonhoire  46832  iunhoiioo  46836  vonioo  46842  vonicc  46845  vonsn  46851  smfpimltxr  46907  smfpimgtxr  46940  smfrec  46949  fmtnoprmfac1  47727  fmtnoprmfac2  47729  lighneallem3  47769  pgn4cyclex  48288