Theorem neqne 2977

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1601   ≠ wne 2969

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 199  df-ne 2970

This theorem is referenced by:  exmidne  2979  2f1fvneq  6791  domwdom  8770  epnsym  8803  dfac2b  9288  fin23lem14  9492  axcc2lem  9595  cshw1  13979  xptrrel  14134  pwm1geoser  15013  dvdsabseq  15452  ncoprmgcdne1b  15779  sgrp2rid2  17811  symg2bas  18212  symgextf  18231  odlem1  18349  gexlem1  18389  cply1mul  20071  psgndiflemB  20353  dmatmul  20719  mdetdiag  20821  mdetunilem9  20842  maducoeval2  20862  madurid  20866  chfacfisf  21077  chfacfisfcpmat  21078  upgriswlk  27005  lfgrwlkprop  27055  2pthnloop  27100  umgr2adedgspth  27345  umgrclwwlkge2  27388  n4cyclfrgr  27716  frgrwopreglem3  27739  frgrregorufr0  27749  bj-rest10b  33623  xppss12  38137  fiiuncl  40179  disjxp1  40183  disjf1  40306  fzisoeu  40437  fzdifsuc2  40447  supxrge  40476  suplesup  40477  infrpge  40489  xrlexaddrp  40490  infleinflem1  40508  infleinflem2  40509  infleinf  40510  xralrple3  40512  fiminre2  40516  xrralrecnnge  40533  infxrpnf  40594  supminfxr  40613  fsumsupp0  40732  limcresiooub  40796  limcresioolb  40797  limclr  40809  climisp  40900  climxlim2lem  40999  dfxlim2v  41001  xlimliminflimsup  41016  icccncfext  41042  cncfiooiccre  41050  dvbdfbdioolem2  41086  ioodvbdlimc1lem2  41089  ioodvbdlimc2lem  41091  dvnxpaek  41099  dvnprodlem3  41105  itgioocnicc  41134  ovolsplit  41146  stoweidlem14  41172  stoweidlem55  41213  stoweid  41221  dirkertrigeqlem3  41258  dirkertrigeq  41259  dirkercncf  41265  fourierdlem9  41274  fourierdlem30  41295  fourierdlem31  41296  fourierdlem33  41298  fourierdlem34  41299  fourierdlem35  41300  fourierdlem42  41307  fourierdlem43  41308  fourierdlem46  41310  fourierdlem48  41312  fourierdlem49  41313  fourierdlem51  41315  fourierdlem54  41318  fourierdlem62  41326  fourierdlem64  41328  fourierdlem65  41329  fourierdlem70  41334  fourierdlem71  41335  fourierdlem73  41337  fourierdlem74  41338  fourierdlem75  41339  fourierdlem76  41340  fourierdlem79  41343  fourierdlem81  41345  fourierdlem82  41346  fourierdlem89  41353  fourierdlem91  41355  fourierdlem102  41366  fourierdlem114  41378  sqwvfoura  41386  fourierswlem  41388  fouriersw  41389  elaa2lem  41391  etransclem25  41417  etransclem28  41420  etransclem35  41427  etransclem38  41430  qndenserrnbl  41453  ioorrnopn  41463  ioorrnopnxrlem  41464  ioorrnopnxr  41465  prsal  41476  issalnnd  41501  sge0cl  41536  sge0pr  41549  sge0prle  41556  sge0isum  41582  sge0xaddlem1  41588  iundjiun  41615  meadjun  41617  ismeannd  41622  caragenfiiuncl  41670  caragenunicl  41679  isomennd  41686  hoicvr  41703  ovnssle  41716  ovn0  41721  ovnsubadd  41727  hoidmvval0b  41745  hoidmvlelem2  41751  hoidmvlelem3  41752  hoidmvle  41755  ovnhoilem1  41756  ovnhoi  41758  ovnlecvr2  41765  hoiqssbl  41780  hspmbllem2  41782  hspmbl  41784  vonhoire  41827  iunhoiioo  41831  vonioo  41837  vonicc  41840  vonsn  41846  smfpimltxr  41897  smfpimgtxr  41929  smfrec  41937  fmtnoprmfac1  42512  fmtnoprmfac2  42514  lighneallem3  42559