Theorem neqne 2940

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

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

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 2933

This theorem is referenced by:  exmidne  2942  domwdom  9489  epnsym  9530  dfac2b  10053  fin23lem14  10255  axcc2lem  10358  fiminre2  12104  cshw1  14784  xptrrel  14942  dvdsabseq  16282  ncoprmgcdne1b  16619  sgrp2rid2  18897  symg2bas  19368  symgextf  19392  odlem1  19510  gexlem1  19554  ablsimpgfind  20087  psgndiflemB  21580  cply1mul  22261  dmatmul  22462  mdetdiag  22564  mdetunilem9  22585  maducoeval2  22605  madurid  22609  chfacfisf  22819  chfacfisfcpmat  22820  plyexmo  26279  aalioulem3  26300  dvradcnv  26386  logtayllem  26623  logtayl  26624  upgriswlk  29709  lfgrwlkprop  29754  2pthnloop  29799  umgr2adedgspth  30016  umgrclwwlkge2  30061  n4cyclfrgr  30361  frgrwopreglem3  30384  frgrregorufr0  30394  domnmuln0rd  33335  elrspunsn  33489  satfv1lem  35544  bj-rest10b  37401  aks6d1c2p2  42558  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  aks6d1c6lem3  42611  aks6d1c7  42623  unitscyglem2  42635  xppss12  42670  sn-0tie0  42896  prjspnfv01  43057  prjspner01  43058  fiiuncl  45496  disjf1  45613  fzisoeu  45733  fzdifsuc2  45743  supxrge  45768  suplesup  45769  infrpge  45781  xrlexaddrp  45782  infleinflem1  45799  infleinflem2  45800  infleinf  45801  xralrple3  45803  xrralrecnnge  45819  infxrpnf  45874  supminfxr  45892  fsumsupp0  46008  limcresiooub  46070  limcresioolb  46071  limclr  46083  climisp  46174  climxlim2lem  46273  dfxlim2v  46275  xlimliminflimsup  46290  icccncfext  46315  cncfiooiccre  46323  dvbdfbdioolem2  46357  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnxpaek  46370  dvnprodlem3  46376  itgioocnicc  46405  ovolsplit  46416  stoweidlem14  46442  stoweidlem55  46483  stoweid  46491  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkercncf  46535  fourierdlem9  46544  fourierdlem30  46565  fourierdlem31  46566  fourierdlem33  46568  fourierdlem34  46569  fourierdlem35  46570  fourierdlem42  46577  fourierdlem43  46578  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem51  46585  fourierdlem54  46588  fourierdlem62  46596  fourierdlem64  46598  fourierdlem65  46599  fourierdlem70  46604  fourierdlem71  46605  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem79  46613  fourierdlem81  46615  fourierdlem82  46616  fourierdlem89  46623  fourierdlem91  46625  fourierdlem102  46636  fourierdlem114  46648  sqwvfoura  46656  fourierswlem  46658  fouriersw  46659  elaa2lem  46661  etransclem25  46687  etransclem28  46690  etransclem35  46697  etransclem38  46700  qndenserrnbl  46723  ioorrnopn  46733  ioorrnopnxrlem  46734  ioorrnopnxr  46735  prsal  46746  issalnnd  46773  sge0cl  46809  sge0pr  46822  sge0prle  46829  sge0isum  46855  sge0xaddlem1  46861  iundjiun  46888  meadjun  46890  ismeannd  46895  caragenfiiuncl  46943  caragenunicl  46952  isomennd  46959  hoicvr  46976  ovnssle  46989  ovn0  46994  ovnsubadd  47000  hoidmvval0b  47018  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvle  47028  ovnhoilem1  47029  ovnhoi  47031  ovnlecvr2  47038  hoiqssbl  47053  hspmbllem2  47055  hspmbl  47057  vonhoire  47100  iunhoiioo  47104  vonioo  47110  vonicc  47113  vonsn  47119  smfpimltxr  47175  smfpimgtxr  47208  smfrec  47217  fmtnoprmfac1  48028  fmtnoprmfac2  48030  lighneallem3  48070  pgn4cyclex  48602