Theorem neqne 2972

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 23	. 2 ⊢ (¬ 𝐴 = 𝐵 → ¬ 𝐴 = 𝐵)
2	1	neqned 2971	1 ⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ≠ wne 2964

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 210  df-ne 2965

This theorem is referenced by:  exmidne  2974  domwdom  9532  epnsym  9574  dfac2b  10110  fin23lem14  10313  axcc2lem  10416  fiminre2  12159  cshw1  14855  xptrrel  15013  dvdsabseq  16367  ncoprmgcdne1b  16704  sgrp2rid2  18984  symg2bas  19459  symgextf  19483  odlem1  19601  gexlem1  19645  ablsimpgfind  20178  psgndiflemB  21715  cply1mul  22421  dmatmul  22619  mdetdiag  22721  mdetunilem9  22742  maducoeval2  22762  madurid  22766  chfacfisf  22976  chfacfisfcpmat  22977  plyexmo  26439  aalioulem3  26460  dvradcnv  26546  logtayllem  26786  logtayl  26787  upgriswlk  29927  lfgrwlkprop  29972  2pthnloop  30017  umgr2adedgspth  30234  umgrclwwlkge2  30279  n4cyclfrgr  30579  frgrwopreglem3  30602  frgrregorufr0  30612  domnmuln0rd  33534  elrspunsn  33677  drnglring  33723  dflringlem3  33727  dflring4  33729  satfv1lem  35749  bj-rest10b  37614  aks6d1c2p2  42771  sticksstones10  42807  sticksstones12a  42809  sticksstones12  42810  aks6d1c6lem3  42824  aks6d1c7  42836  unitscyglem2  42848  xppss12  42883  sn-0tie0  43108  prjspnfv01  43241  prjspner01  43242  fiiuncl  45670  disjf1  45786  fzisoeu  45904  fzdifsuc2  45914  supxrge  45939  suplesup  45940  infrpge  45952  xrlexaddrp  45953  infleinflem1  45970  infleinflem2  45971  infleinf  45972  xralrple3  45974  xrralrecnnge  45990  infxrpnf  46045  supminfxr  46063  fsumsupp0  46179  limcresiooub  46241  limcresioolb  46242  limclr  46254  climisp  46345  climxlim2lem  46444  dfxlim2v  46446  xlimliminflimsup  46461  icccncfext  46486  cncfiooiccre  46494  dvbdfbdioolem2  46528  ioodvbdlimc1lem2  46531  ioodvbdlimc2lem  46533  dvnxpaek  46541  dvnprodlem3  46547  itgioocnicc  46576  ovolsplit  46587  stoweidlem14  46613  stoweidlem55  46654  stoweid  46662  dirkertrigeqlem3  46699  dirkertrigeq  46700  dirkercncf  46706  fourierdlem9  46715  fourierdlem30  46736  fourierdlem31  46737  fourierdlem33  46739  fourierdlem34  46740  fourierdlem35  46741  fourierdlem42  46748  fourierdlem43  46749  fourierdlem46  46751  fourierdlem48  46753  fourierdlem49  46754  fourierdlem51  46756  fourierdlem54  46759  fourierdlem62  46767  fourierdlem64  46769  fourierdlem65  46770  fourierdlem70  46775  fourierdlem71  46776  fourierdlem73  46778  fourierdlem74  46779  fourierdlem75  46780  fourierdlem76  46781  fourierdlem79  46784  fourierdlem81  46786  fourierdlem82  46787  fourierdlem89  46794  fourierdlem91  46796  fourierdlem102  46807  fourierdlem114  46819  sqwvfoura  46827  fourierswlem  46829  fouriersw  46830  elaa2lem  46832  etransclem25  46858  etransclem28  46861  etransclem35  46868  etransclem38  46871  qndenserrnbl  46894  ioorrnopn  46904  ioorrnopnxrlem  46905  ioorrnopnxr  46906  prsal  46917  issalnnd  46944  sge0cl  46980  sge0pr  46993  sge0prle  47000  sge0isum  47026  sge0xaddlem1  47032  iundjiun  47059  meadjun  47061  ismeannd  47066  caragenfiiuncl  47114  caragenunicl  47123  isomennd  47130  hoicvr  47147  ovnssle  47160  ovn0  47165  ovnsubadd  47171  hoidmvval0b  47189  hoidmvlelem2  47195  hoidmvlelem3  47196  hoidmvle  47199  ovnhoilem1  47200  ovnhoi  47202  ovnlecvr2  47209  hoiqssbl  47224  hspmbllem2  47226  hspmbl  47228  vonhoire  47271  iunhoiioo  47275  vonioo  47281  vonicc  47284  vonsn  47290  smfpimltxr  47346  smfpimgtxr  47379  smfrec  47388  fmtnoprmfac1  48199  fmtnoprmfac2  48201  lighneallem3  48241  pgn4cyclex  48773