Theorem neqne 2790

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  exmidne  2792  pwm1geoser  14439  dvdsabseq  14873  zeneo  14901  bj-rest10b  32223  fiiuncl  38259  disjxp1  38263  disjf1  38364  fzisoeu  38455  fzdifsuc2  38466  supxrge  38495  suplesup  38496  infrpge  38508  xrlexaddrp  38509  infleinflem1  38527  infleinflem2  38528  infleinf  38529  xralrple3  38531  fiminre2  38535  xrralrecnnge  38554  fsumsupp0  38645  limcresiooub  38709  limcresioolb  38710  limclr  38722  icccncfext  38773  cncfiooiccre  38781  dvbdfbdioolem2  38819  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnxpaek  38832  dvnprodlem3  38838  itgioocnicc  38869  ovolsplit  38881  stoweidlem14  38907  stoweidlem55  38948  stoweid  38956  dirkertrigeqlem3  38993  dirkertrigeq  38994  dirkercncf  39000  fourierdlem9  39009  fourierdlem30  39030  fourierdlem31  39031  fourierdlem33  39033  fourierdlem34  39034  fourierdlem35  39035  fourierdlem42  39042  fourierdlem43  39043  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem51  39050  fourierdlem54  39053  fourierdlem62  39061  fourierdlem64  39063  fourierdlem65  39064  fourierdlem70  39069  fourierdlem71  39070  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem79  39078  fourierdlem81  39080  fourierdlem82  39081  fourierdlem89  39088  fourierdlem91  39090  fourierdlem102  39101  fourierdlem114  39113  sqwvfoura  39121  fourierswlem  39123  fouriersw  39124  elaa2lem  39126  etransclem25  39152  etransclem28  39155  etransclem35  39162  etransclem38  39165  qndenserrnbl  39191  ioorrnopn  39201  ioorrnopnxrlem  39202  ioorrnopnxr  39203  prsal  39214  issalnnd  39239  sge0cl  39274  sge0pr  39287  sge0prle  39294  sge0isum  39320  sge0xaddlem1  39326  iundjiun  39353  meadjun  39355  ismeannd  39360  caragenfiiuncl  39405  caragenunicl  39414  isomennd  39421  hoicvr  39438  ovnssle  39451  ovn0  39456  ovnsubadd  39462  hoidmvval0b  39480  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvle  39490  ovnhoilem1  39491  ovnhoi  39493  ovnlecvr2  39500  hoiqssbl  39515  hspmbllem2  39517  hspmbl  39519  vonhoire  39563  iunhoiioo  39567  vonioo  39573  vonicc  39576  vonsn  39582  smfpimltxr  39634  smfpimgtxr  39666  smfrec  39674  fmtnoprmfac1  40015  fmtnoprmfac2  40017  lighneallem3  40062  lfgrwlkprop  40896  2pthnloop  40937  umgr2adedgspth  41155  clwwlknclwwlkdifs  41181  umgrclwwlksge2  41219  n4cyclfrgr  41461  frgrwopreglem3  41483  frgrregorufr0  41489