Theorem neqne 2936

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

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

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 2929

This theorem is referenced by:  exmidne  2938  domwdom  9455  epnsym  9494  dfac2b  10017  fin23lem14  10219  axcc2lem  10322  fiminre2  12065  cshw1  14724  xptrrel  14882  dvdsabseq  16219  ncoprmgcdne1b  16556  sgrp2rid2  18829  symg2bas  19300  symgextf  19324  odlem1  19442  gexlem1  19486  ablsimpgfind  20019  psgndiflemB  21532  cply1mul  22206  dmatmul  22407  mdetdiag  22509  mdetunilem9  22530  maducoeval2  22550  madurid  22554  chfacfisf  22764  chfacfisfcpmat  22765  plyexmo  26243  aalioulem3  26264  dvradcnv  26352  logtayllem  26590  logtayl  26591  upgriswlk  29614  lfgrwlkprop  29659  2pthnloop  29704  umgr2adedgspth  29921  umgrclwwlkge2  29963  n4cyclfrgr  30263  frgrwopreglem3  30286  frgrregorufr0  30296  domnmuln0rd  33233  elrspunsn  33386  satfv1lem  35398  bj-rest10b  37123  aks6d1c2p2  42152  sticksstones10  42188  sticksstones12a  42190  sticksstones12  42191  aks6d1c6lem3  42205  aks6d1c7  42217  unitscyglem2  42229  xppss12  42262  sn-0tie0  42484  prjspnfv01  42657  prjspner01  42658  fiiuncl  45102  disjf1  45220  fzisoeu  45341  fzdifsuc2  45351  supxrge  45377  suplesup  45378  infrpge  45390  xrlexaddrp  45391  infleinflem1  45408  infleinflem2  45409  infleinf  45410  xralrple3  45412  xrralrecnnge  45428  infxrpnf  45484  supminfxr  45502  fsumsupp0  45618  limcresiooub  45680  limcresioolb  45681  limclr  45693  climisp  45784  climxlim2lem  45883  dfxlim2v  45885  xlimliminflimsup  45900  icccncfext  45925  cncfiooiccre  45933  dvbdfbdioolem2  45967  ioodvbdlimc1lem2  45970  ioodvbdlimc2lem  45972  dvnxpaek  45980  dvnprodlem3  45986  itgioocnicc  46015  ovolsplit  46026  stoweidlem14  46052  stoweidlem55  46093  stoweid  46101  dirkertrigeqlem3  46138  dirkertrigeq  46139  dirkercncf  46145  fourierdlem9  46154  fourierdlem30  46175  fourierdlem31  46176  fourierdlem33  46178  fourierdlem34  46179  fourierdlem35  46180  fourierdlem42  46187  fourierdlem43  46188  fourierdlem46  46190  fourierdlem48  46192  fourierdlem49  46193  fourierdlem51  46195  fourierdlem54  46198  fourierdlem62  46206  fourierdlem64  46208  fourierdlem65  46209  fourierdlem70  46214  fourierdlem71  46215  fourierdlem73  46217  fourierdlem74  46218  fourierdlem75  46219  fourierdlem76  46220  fourierdlem79  46223  fourierdlem81  46225  fourierdlem82  46226  fourierdlem89  46233  fourierdlem91  46235  fourierdlem102  46246  fourierdlem114  46258  sqwvfoura  46266  fourierswlem  46268  fouriersw  46269  elaa2lem  46271  etransclem25  46297  etransclem28  46300  etransclem35  46307  etransclem38  46310  qndenserrnbl  46333  ioorrnopn  46343  ioorrnopnxrlem  46344  ioorrnopnxr  46345  prsal  46356  issalnnd  46383  sge0cl  46419  sge0pr  46432  sge0prle  46439  sge0isum  46465  sge0xaddlem1  46471  iundjiun  46498  meadjun  46500  ismeannd  46505  caragenfiiuncl  46553  caragenunicl  46562  isomennd  46569  hoicvr  46586  ovnssle  46599  ovn0  46604  ovnsubadd  46610  hoidmvval0b  46628  hoidmvlelem2  46634  hoidmvlelem3  46635  hoidmvle  46638  ovnhoilem1  46639  ovnhoi  46641  ovnlecvr2  46648  hoiqssbl  46663  hspmbllem2  46665  hspmbl  46667  vonhoire  46710  iunhoiioo  46714  vonioo  46720  vonicc  46723  vonsn  46729  smfpimltxr  46785  smfpimgtxr  46818  smfrec  46827  fmtnoprmfac1  47596  fmtnoprmfac2  47598  lighneallem3  47638  pgn4cyclex  48157