Theorem neqne 2940

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2932

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 2933

This theorem is referenced by:  exmidne  2942  domwdom  9479  epnsym  9518  dfac2b  10041  fin23lem14  10243  axcc2lem  10346  fiminre2  12090  cshw1  14745  xptrrel  14903  dvdsabseq  16240  ncoprmgcdne1b  16577  sgrp2rid2  18851  symg2bas  19322  symgextf  19346  odlem1  19464  gexlem1  19508  ablsimpgfind  20041  psgndiflemB  21555  cply1mul  22240  dmatmul  22441  mdetdiag  22543  mdetunilem9  22564  maducoeval2  22584  madurid  22588  chfacfisf  22798  chfacfisfcpmat  22799  plyexmo  26277  aalioulem3  26298  dvradcnv  26386  logtayllem  26624  logtayl  26625  upgriswlk  29714  lfgrwlkprop  29759  2pthnloop  29804  umgr2adedgspth  30021  umgrclwwlkge2  30066  n4cyclfrgr  30366  frgrwopreglem3  30389  frgrregorufr0  30399  domnmuln0rd  33356  elrspunsn  33510  satfv1lem  35556  bj-rest10b  37294  aks6d1c2p2  42373  sticksstones10  42409  sticksstones12a  42411  sticksstones12  42412  aks6d1c6lem3  42426  aks6d1c7  42438  unitscyglem2  42450  xppss12  42485  sn-0tie0  42706  prjspnfv01  42867  prjspner01  42868  fiiuncl  45310  disjf1  45427  fzisoeu  45548  fzdifsuc2  45558  supxrge  45583  suplesup  45584  infrpge  45596  xrlexaddrp  45597  infleinflem1  45614  infleinflem2  45615  infleinf  45616  xralrple3  45618  xrralrecnnge  45634  infxrpnf  45690  supminfxr  45708  fsumsupp0  45824  limcresiooub  45886  limcresioolb  45887  limclr  45899  climisp  45990  climxlim2lem  46089  dfxlim2v  46091  xlimliminflimsup  46106  icccncfext  46131  cncfiooiccre  46139  dvbdfbdioolem2  46173  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnxpaek  46186  dvnprodlem3  46192  itgioocnicc  46221  ovolsplit  46232  stoweidlem14  46258  stoweidlem55  46299  stoweid  46307  dirkertrigeqlem3  46344  dirkertrigeq  46345  dirkercncf  46351  fourierdlem9  46360  fourierdlem30  46381  fourierdlem31  46382  fourierdlem33  46384  fourierdlem34  46385  fourierdlem35  46386  fourierdlem42  46393  fourierdlem43  46394  fourierdlem46  46396  fourierdlem48  46398  fourierdlem49  46399  fourierdlem51  46401  fourierdlem54  46404  fourierdlem62  46412  fourierdlem64  46414  fourierdlem65  46415  fourierdlem70  46420  fourierdlem71  46421  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem76  46426  fourierdlem79  46429  fourierdlem81  46431  fourierdlem82  46432  fourierdlem89  46439  fourierdlem91  46441  fourierdlem102  46452  fourierdlem114  46464  sqwvfoura  46472  fourierswlem  46474  fouriersw  46475  elaa2lem  46477  etransclem25  46503  etransclem28  46506  etransclem35  46513  etransclem38  46516  qndenserrnbl  46539  ioorrnopn  46549  ioorrnopnxrlem  46550  ioorrnopnxr  46551  prsal  46562  issalnnd  46589  sge0cl  46625  sge0pr  46638  sge0prle  46645  sge0isum  46671  sge0xaddlem1  46677  iundjiun  46704  meadjun  46706  ismeannd  46711  caragenfiiuncl  46759  caragenunicl  46768  isomennd  46775  hoicvr  46792  ovnssle  46805  ovn0  46810  ovnsubadd  46816  hoidmvval0b  46834  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvle  46844  ovnhoilem1  46845  ovnhoi  46847  ovnlecvr2  46854  hoiqssbl  46869  hspmbllem2  46871  hspmbl  46873  vonhoire  46916  iunhoiioo  46920  vonioo  46926  vonicc  46929  vonsn  46935  smfpimltxr  46991  smfpimgtxr  47024  smfrec  47033  fmtnoprmfac1  47811  fmtnoprmfac2  47813  lighneallem3  47853  pgn4cyclex  48372