Theorem neqne 2964

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

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

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 2957

This theorem is used by:  exmidne  2966  domwdom  9561  epnsym  9603  dfac2b  10202  fin23lem14  10404  axcc2lem  10507  fiminre2  12258  cshw1  14966  xptrrel  15126  dvdsabseq  16476  ncoprmgcdne1b  16818  sgrp2rid2  19118  symg2bas  19600  symgextf  19624  odlem1  19742  gexlem1  19786  ablsimpgfind  20319  psgndiflemB  21899  cply1mul  22607  dmatmul  22805  mdetdiag  22907  mdetunilem9  22928  maducoeval2  22948  madurid  22952  chfacfisf  23165  chfacfisfcpmat  23166  plyexmo  26629  aalioulem3  26654  dvradcnv  26741  logtayllem  26980  logtayl  26981  upgriswlk  30214  lfgrwlkprop  30263  2pthnloop  30310  umgr2adedgspth  30530  umgrclwwlkge2  30575  n4cyclfrgr  30885  frgrwopreglem3  30908  frgrregorufr0  30918  domnmuln0rd  33831  elrspunsn  33972  drnglring  34017  dflringlem3  34021  dflring4  34023  satfv1lem  36106  bj-rest10b  37990  aks6d1c2p2  43149  sticksstones10  43185  sticksstones12a  43187  sticksstones12  43188  aks6d1c6lem3  43202  aks6d1c7  43214  unitscyglem2  43226  xppss12  43263  sn-0tie0  43495  fiiuncl  46051  disjf1  46167  fzisoeu  46285  fzdifsuc2  46295  supxrge  46319  suplesup  46320  infrpge  46332  xrlexaddrp  46333  infleinflem1  46350  infleinflem2  46351  infleinf  46352  xralrple3  46354  xrralrecnnge  46370  infxrpnf  46425  supminfxr  46443  fsumsupp0  46559  limcresiooub  46621  limcresioolb  46622  limclr  46634  climisp  46725  climxlim2lem  46824  dfxlim2v  46826  xlimliminflimsup  46841  icccncfext  46866  cncfiooiccre  46874  dvbdfbdioolem2  46908  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  dvnxpaek  46921  dvnprodlem3  46927  itgioocnicc  46956  ovolsplit  46967  stoweidlem14  46993  stoweidlem55  47034  stoweid  47042  dirkertrigeqlem3  47079  dirkertrigeq  47080  dirkercncf  47086  fourierdlem9  47095  fourierdlem30  47116  fourierdlem31  47117  fourierdlem33  47119  fourierdlem34  47120  fourierdlem35  47121  fourierdlem42  47128  fourierdlem43  47129  fourierdlem46  47131  fourierdlem48  47133  fourierdlem49  47134  fourierdlem51  47136  fourierdlem54  47139  fourierdlem62  47147  fourierdlem64  47149  fourierdlem65  47150  fourierdlem70  47155  fourierdlem71  47156  fourierdlem73  47158  fourierdlem74  47159  fourierdlem75  47160  fourierdlem76  47161  fourierdlem79  47164  fourierdlem81  47166  fourierdlem82  47167  fourierdlem89  47174  fourierdlem91  47176  fourierdlem102  47187  fourierdlem114  47199  sqwvfoura  47207  fourierswlem  47209  fouriersw  47210  elaa2lem  47212  etransclem25  47238  etransclem28  47241  etransclem35  47248  etransclem38  47251  qndenserrnbl  47274  ioorrnopn  47284  ioorrnopnxrlem  47285  ioorrnopnxr  47286  prsal  47297  issalnnd  47324  sge0cl  47360  sge0pr  47373  sge0prle  47380  sge0isum  47406  sge0xaddlem1  47412  iundjiun  47439  meadjun  47441  ismeannd  47446  caragenfiiuncl  47494  caragenunicl  47503  isomennd  47510  hoicvr  47527  ovnssle  47540  ovn0  47545  ovnsubadd  47551  hoidmvval0b  47569  hoidmvlelem2  47575  hoidmvlelem3  47576  hoidmvle  47579  ovnhoilem1  47580  ovnhoi  47582  ovnlecvr2  47589  hoiqssbl  47604  hspmbllem2  47606  hspmbl  47608  vonhoire  47651  iunhoiioo  47655  vonioo  47661  vonicc  47664  vonsn  47670  smfpimltxr  47726  smfpimgtxr  47759  smfrec  47768  fmtnoprmfac1  48619  fmtnoprmfac2  48621  lighneallem3  48661  pgn4cyclex  49193