Theorem neqne 2963

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  exmidne  2965  domwdom  9572  epnsym  9614  dfac2b  10213  fin23lem14  10415  axcc2lem  10518  fiminre2  12269  cshw1  14978  xptrrel  15139  dvdsabseq  16489  ncoprmgcdne1b  16831  sgrp2rid2  19131  symg2bas  19613  symgextf  19637  odlem1  19755  gexlem1  19799  ablsimpgfind  20332  psgndiflemB  21912  cply1mul  22620  dmatmul  22818  mdetdiag  22920  mdetunilem9  22941  maducoeval2  22961  madurid  22965  chfacfisf  23178  chfacfisfcpmat  23179  plyexmo  26642  aalioulem3  26667  dvradcnv  26754  logtayllem  26993  logtayl  26994  upgriswlk  30227  lfgrwlkprop  30276  2pthnloop  30323  umgr2adedgspth  30543  umgrclwwlkge2  30588  n4cyclfrgr  30898  frgrwopreglem3  30921  frgrregorufr0  30931  domnmuln0rd  33885  elrspunsn  34026  drnglring  34071  dflringlem3  34075  dflring4  34077  satfv1lem  36214  bj-rest10b  38103  aks6d1c2p2  43263  sticksstones10  43299  sticksstones12a  43301  sticksstones12  43302  aks6d1c6lem3  43316  aks6d1c7  43328  unitscyglem2  43340  xppss12  43377  sn-0tie0  43609  fiiuncl  46176  disjf1  46292  fzisoeu  46410  fzdifsuc2  46420  supxrge  46444  suplesup  46445  infrpge  46457  xrlexaddrp  46458  infleinflem1  46475  infleinflem2  46476  infleinf  46477  xralrple3  46479  xrralrecnnge  46495  infxrpnf  46550  supminfxr  46568  fsumsupp0  46684  limcresiooub  46746  limcresioolb  46747  limclr  46759  climisp  46850  climxlim2lem  46949  dfxlim2v  46951  xlimliminflimsup  46966  icccncfext  46991  cncfiooiccre  46999  dvbdfbdioolem2  47033  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  dvnxpaek  47046  dvnprodlem3  47052  itgioocnicc  47081  ovolsplit  47092  stoweidlem14  47118  stoweidlem55  47159  stoweid  47167  dirkertrigeqlem3  47204  dirkertrigeq  47205  dirkercncf  47211  fourierdlem9  47220  fourierdlem30  47241  fourierdlem31  47242  fourierdlem33  47244  fourierdlem34  47245  fourierdlem35  47246  fourierdlem42  47253  fourierdlem43  47254  fourierdlem46  47256  fourierdlem48  47258  fourierdlem49  47259  fourierdlem51  47261  fourierdlem54  47264  fourierdlem62  47272  fourierdlem64  47274  fourierdlem65  47275  fourierdlem70  47280  fourierdlem71  47281  fourierdlem73  47283  fourierdlem74  47284  fourierdlem75  47285  fourierdlem76  47286  fourierdlem79  47289  fourierdlem81  47291  fourierdlem82  47292  fourierdlem89  47299  fourierdlem91  47301  fourierdlem102  47312  fourierdlem114  47324  sqwvfoura  47332  fourierswlem  47334  fouriersw  47335  elaa2lem  47337  etransclem25  47363  etransclem28  47366  etransclem35  47373  etransclem38  47376  qndenserrnbl  47399  ioorrnopn  47409  ioorrnopnxrlem  47410  ioorrnopnxr  47411  prsal  47422  issalnnd  47449  sge0cl  47485  sge0pr  47498  sge0prle  47505  sge0isum  47531  sge0xaddlem1  47537  iundjiun  47564  meadjun  47566  ismeannd  47571  caragenfiiuncl  47619  caragenunicl  47628  isomennd  47635  hoicvr  47652  ovnssle  47665  ovn0  47670  ovnsubadd  47676  hoidmvval0b  47694  hoidmvlelem2  47700  hoidmvlelem3  47701  hoidmvle  47704  ovnhoilem1  47705  ovnhoi  47707  ovnlecvr2  47714  hoiqssbl  47729  hspmbllem2  47731  hspmbl  47733  vonhoire  47776  iunhoiioo  47780  vonioo  47786  vonicc  47789  vonsn  47795  smfpimltxr  47851  smfpimgtxr  47884  smfrec  47893  fmtnoprmfac1  48744  fmtnoprmfac2  48746  lighneallem3  48786  pgn4cyclex  49318