Theorem neqne 2941

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

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

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 2934

This theorem is referenced by:  exmidne  2943  domwdom  9482  epnsym  9521  dfac2b  10044  fin23lem14  10246  axcc2lem  10349  fiminre2  12095  cshw1  14775  xptrrel  14933  dvdsabseq  16273  ncoprmgcdne1b  16610  sgrp2rid2  18888  symg2bas  19359  symgextf  19383  odlem1  19501  gexlem1  19545  ablsimpgfind  20078  psgndiflemB  21590  cply1mul  22271  dmatmul  22472  mdetdiag  22574  mdetunilem9  22595  maducoeval2  22615  madurid  22619  chfacfisf  22829  chfacfisfcpmat  22830  plyexmo  26290  aalioulem3  26311  dvradcnv  26399  logtayllem  26636  logtayl  26637  upgriswlk  29724  lfgrwlkprop  29769  2pthnloop  29814  umgr2adedgspth  30031  umgrclwwlkge2  30076  n4cyclfrgr  30376  frgrwopreglem3  30399  frgrregorufr0  30409  domnmuln0rd  33350  elrspunsn  33504  satfv1lem  35560  bj-rest10b  37417  aks6d1c2p2  42572  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  aks6d1c6lem3  42625  aks6d1c7  42637  unitscyglem2  42649  xppss12  42684  sn-0tie0  42910  prjspnfv01  43071  prjspner01  43072  fiiuncl  45514  disjf1  45631  fzisoeu  45751  fzdifsuc2  45761  supxrge  45786  suplesup  45787  infrpge  45799  xrlexaddrp  45800  infleinflem1  45817  infleinflem2  45818  infleinf  45819  xralrple3  45821  xrralrecnnge  45837  infxrpnf  45892  supminfxr  45910  fsumsupp0  46026  limcresiooub  46088  limcresioolb  46089  limclr  46101  climisp  46192  climxlim2lem  46291  dfxlim2v  46293  xlimliminflimsup  46308  icccncfext  46333  cncfiooiccre  46341  dvbdfbdioolem2  46375  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnxpaek  46388  dvnprodlem3  46394  itgioocnicc  46423  ovolsplit  46434  stoweidlem14  46460  stoweidlem55  46501  stoweid  46509  dirkertrigeqlem3  46546  dirkertrigeq  46547  dirkercncf  46553  fourierdlem9  46562  fourierdlem30  46583  fourierdlem31  46584  fourierdlem33  46586  fourierdlem34  46587  fourierdlem35  46588  fourierdlem42  46595  fourierdlem43  46596  fourierdlem46  46598  fourierdlem48  46600  fourierdlem49  46601  fourierdlem51  46603  fourierdlem54  46606  fourierdlem62  46614  fourierdlem64  46616  fourierdlem65  46617  fourierdlem70  46622  fourierdlem71  46623  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem79  46631  fourierdlem81  46633  fourierdlem82  46634  fourierdlem89  46641  fourierdlem91  46643  fourierdlem102  46654  fourierdlem114  46666  sqwvfoura  46674  fourierswlem  46676  fouriersw  46677  elaa2lem  46679  etransclem25  46705  etransclem28  46708  etransclem35  46715  etransclem38  46718  qndenserrnbl  46741  ioorrnopn  46751  ioorrnopnxrlem  46752  ioorrnopnxr  46753  prsal  46764  issalnnd  46791  sge0cl  46827  sge0pr  46840  sge0prle  46847  sge0isum  46873  sge0xaddlem1  46879  iundjiun  46906  meadjun  46908  ismeannd  46913  caragenfiiuncl  46961  caragenunicl  46970  isomennd  46977  hoicvr  46994  ovnssle  47007  ovn0  47012  ovnsubadd  47018  hoidmvval0b  47036  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvle  47046  ovnhoilem1  47047  ovnhoi  47049  ovnlecvr2  47056  hoiqssbl  47071  hspmbllem2  47073  hspmbl  47075  vonhoire  47118  iunhoiioo  47122  vonioo  47128  vonicc  47131  vonsn  47137  smfpimltxr  47193  smfpimgtxr  47226  smfrec  47235  fmtnoprmfac1  48040  fmtnoprmfac2  48042  lighneallem3  48082  pgn4cyclex  48614