Theorem neqne 2949

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2941

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 2942

This theorem is referenced by:  exmidne  2951  2f1fvneq  7259  domwdom  9569  epnsym  9604  dfac2b  10125  fin23lem14  10328  axcc2lem  10431  fiminre2  12162  cshw1  14772  xptrrel  14927  dvdsabseq  16256  ncoprmgcdne1b  16587  sgrp2rid2  18807  symg2bas  19260  symgextf  19285  odlem1  19403  gexlem1  19447  ablsimpgfind  19980  psgndiflemB  21153  cply1mul  21818  dmatmul  21999  mdetdiag  22101  mdetunilem9  22122  maducoeval2  22142  madurid  22146  chfacfisf  22356  chfacfisfcpmat  22357  plyexmo  25826  aalioulem3  25847  dvradcnv  25933  logtayllem  26167  logtayl  26168  upgriswlk  28898  lfgrwlkprop  28944  2pthnloop  28988  umgr2adedgspth  29202  umgrclwwlkge2  29244  n4cyclfrgr  29544  frgrwopreglem3  29567  frgrregorufr0  29577  elrspunsn  32547  satfv1lem  34353  bj-rest10b  35970  aks6d1c2p2  40957  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  metakunt2  40986  xppss12  41047  sn-0tie0  41312  prjspnfv01  41366  prjspner01  41367  fiiuncl  43752  disjf1  43880  fzisoeu  44010  fzdifsuc2  44020  supxrge  44048  suplesup  44049  infrpge  44061  xrlexaddrp  44062  infleinflem1  44080  infleinflem2  44081  infleinf  44082  xralrple3  44084  xrralrecnnge  44100  infxrpnf  44156  supminfxr  44174  fsumsupp0  44294  limcresiooub  44358  limcresioolb  44359  limclr  44371  climisp  44462  climxlim2lem  44561  dfxlim2v  44563  xlimliminflimsup  44578  icccncfext  44603  cncfiooiccre  44611  dvbdfbdioolem2  44645  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnxpaek  44658  dvnprodlem3  44664  itgioocnicc  44693  ovolsplit  44704  stoweidlem14  44730  stoweidlem55  44771  stoweid  44779  dirkertrigeqlem3  44816  dirkertrigeq  44817  dirkercncf  44823  fourierdlem9  44832  fourierdlem30  44853  fourierdlem31  44854  fourierdlem33  44856  fourierdlem34  44857  fourierdlem35  44858  fourierdlem42  44865  fourierdlem43  44866  fourierdlem46  44868  fourierdlem48  44870  fourierdlem49  44871  fourierdlem51  44873  fourierdlem54  44876  fourierdlem62  44884  fourierdlem64  44886  fourierdlem65  44887  fourierdlem70  44892  fourierdlem71  44893  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem79  44901  fourierdlem81  44903  fourierdlem82  44904  fourierdlem89  44911  fourierdlem91  44913  fourierdlem102  44924  fourierdlem114  44936  sqwvfoura  44944  fourierswlem  44946  fouriersw  44947  elaa2lem  44949  etransclem25  44975  etransclem28  44978  etransclem35  44985  etransclem38  44988  qndenserrnbl  45011  ioorrnopn  45021  ioorrnopnxrlem  45022  ioorrnopnxr  45023  prsal  45034  issalnnd  45061  sge0cl  45097  sge0pr  45110  sge0prle  45117  sge0isum  45143  sge0xaddlem1  45149  iundjiun  45176  meadjun  45178  ismeannd  45183  caragenfiiuncl  45231  caragenunicl  45240  isomennd  45247  hoicvr  45264  ovnssle  45277  ovn0  45282  ovnsubadd  45288  hoidmvval0b  45306  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvle  45316  ovnhoilem1  45317  ovnhoi  45319  ovnlecvr2  45326  hoiqssbl  45341  hspmbllem2  45343  hspmbl  45345  vonhoire  45388  iunhoiioo  45392  vonioo  45398  vonicc  45401  vonsn  45407  smfpimltxr  45463  smfpimgtxr  45496  smfrec  45505  fmtnoprmfac1  46233  fmtnoprmfac2  46235  lighneallem3  46275