Theorem neqne 2968

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

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

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 2961

This theorem is used by:  exmidne  2970  domwdom  9539  epnsym  9581  dfac2b  10126  fin23lem14  10328  axcc2lem  10431  fiminre2  12174  cshw1  14878  xptrrel  15036  dvdsabseq  16388  ncoprmgcdne1b  16725  sgrp2rid2  19011  symg2bas  19486  symgextf  19510  odlem1  19628  gexlem1  19672  ablsimpgfind  20205  psgndiflemB  21779  cply1mul  22485  dmatmul  22683  mdetdiag  22785  mdetunilem9  22806  maducoeval2  22826  madurid  22830  chfacfisf  23040  chfacfisfcpmat  23041  plyexmo  26503  aalioulem3  26526  dvradcnv  26613  logtayllem  26853  logtayl  26854  upgriswlk  30019  lfgrwlkprop  30064  2pthnloop  30109  umgr2adedgspth  30326  umgrclwwlkge2  30371  n4cyclfrgr  30671  frgrwopreglem3  30694  frgrregorufr0  30704  domnmuln0rd  33620  elrspunsn  33760  drnglring  33805  dflringlem3  33809  dflring4  33811  satfv1lem  35867  bj-rest10b  37764  aks6d1c2p2  42919  sticksstones10  42955  sticksstones12a  42957  sticksstones12  42958  aks6d1c6lem3  42972  aks6d1c7  42984  unitscyglem2  42996  xppss12  43033  sn-0tie0  43258  prjspnfv01  43389  prjspner01  43390  fiiuncl  45818  disjf1  45934  fzisoeu  46052  fzdifsuc2  46062  supxrge  46087  suplesup  46088  infrpge  46100  xrlexaddrp  46101  infleinflem1  46118  infleinflem2  46119  infleinf  46120  xralrple3  46122  xrralrecnnge  46138  infxrpnf  46193  supminfxr  46211  fsumsupp0  46327  limcresiooub  46389  limcresioolb  46390  limclr  46402  climisp  46493  climxlim2lem  46592  dfxlim2v  46594  xlimliminflimsup  46609  icccncfext  46634  cncfiooiccre  46642  dvbdfbdioolem2  46676  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  dvnxpaek  46689  dvnprodlem3  46695  itgioocnicc  46724  ovolsplit  46735  stoweidlem14  46761  stoweidlem55  46802  stoweid  46810  dirkertrigeqlem3  46847  dirkertrigeq  46848  dirkercncf  46854  fourierdlem9  46863  fourierdlem30  46884  fourierdlem31  46885  fourierdlem33  46887  fourierdlem34  46888  fourierdlem35  46889  fourierdlem42  46896  fourierdlem43  46897  fourierdlem46  46899  fourierdlem48  46901  fourierdlem49  46902  fourierdlem51  46904  fourierdlem54  46907  fourierdlem62  46915  fourierdlem64  46917  fourierdlem65  46918  fourierdlem70  46923  fourierdlem71  46924  fourierdlem73  46926  fourierdlem74  46927  fourierdlem75  46928  fourierdlem76  46929  fourierdlem79  46932  fourierdlem81  46934  fourierdlem82  46935  fourierdlem89  46942  fourierdlem91  46944  fourierdlem102  46955  fourierdlem114  46967  sqwvfoura  46975  fourierswlem  46977  fouriersw  46978  elaa2lem  46980  etransclem25  47006  etransclem28  47009  etransclem35  47016  etransclem38  47019  qndenserrnbl  47042  ioorrnopn  47052  ioorrnopnxrlem  47053  ioorrnopnxr  47054  prsal  47065  issalnnd  47092  sge0cl  47128  sge0pr  47141  sge0prle  47148  sge0isum  47174  sge0xaddlem1  47180  iundjiun  47207  meadjun  47209  ismeannd  47214  caragenfiiuncl  47262  caragenunicl  47271  isomennd  47278  hoicvr  47295  ovnssle  47308  ovn0  47313  ovnsubadd  47319  hoidmvval0b  47337  hoidmvlelem2  47343  hoidmvlelem3  47344  hoidmvle  47347  ovnhoilem1  47348  ovnhoi  47350  ovnlecvr2  47357  hoiqssbl  47372  hspmbllem2  47374  hspmbl  47376  vonhoire  47419  iunhoiioo  47423  vonioo  47429  vonicc  47432  vonsn  47438  smfpimltxr  47494  smfpimgtxr  47527  smfrec  47536  fmtnoprmfac1  48350  fmtnoprmfac2  48352  lighneallem3  48392  pgn4cyclex  48924