Theorem neqne 2947

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

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

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 206  df-ne 2940

This theorem is referenced by:  exmidne  2949  2f1fvneq  7212  domwdom  9519  epnsym  9554  dfac2b  10075  fin23lem14  10278  axcc2lem  10381  fiminre2  12112  cshw1  14722  xptrrel  14877  dvdsabseq  16206  ncoprmgcdne1b  16537  sgrp2rid2  18750  symg2bas  19188  symgextf  19213  odlem1  19331  gexlem1  19375  ablsimpgfind  19903  psgndiflemB  21041  cply1mul  21702  dmatmul  21883  mdetdiag  21985  mdetunilem9  22006  maducoeval2  22026  madurid  22030  chfacfisf  22240  chfacfisfcpmat  22241  plyexmo  25710  aalioulem3  25731  dvradcnv  25817  logtayllem  26051  logtayl  26052  upgriswlk  28652  lfgrwlkprop  28698  2pthnloop  28742  umgr2adedgspth  28956  umgrclwwlkge2  28998  n4cyclfrgr  29298  frgrwopreglem3  29321  frgrregorufr0  29331  satfv1lem  34043  bj-rest10b  35633  aks6d1c2p2  40622  sticksstones10  40636  sticksstones12a  40638  sticksstones12  40639  metakunt2  40651  xppss12  40723  sn-0tie0  40966  prjspnfv01  41020  prjspner01  41021  fiiuncl  43395  disjf1  43523  fzisoeu  43655  fzdifsuc2  43665  supxrge  43693  suplesup  43694  infrpge  43706  xrlexaddrp  43707  infleinflem1  43725  infleinflem2  43726  infleinf  43727  xralrple3  43729  xrralrecnnge  43745  infxrpnf  43801  supminfxr  43819  fsumsupp0  43939  limcresiooub  44003  limcresioolb  44004  limclr  44016  climisp  44107  climxlim2lem  44206  dfxlim2v  44208  xlimliminflimsup  44223  icccncfext  44248  cncfiooiccre  44256  dvbdfbdioolem2  44290  ioodvbdlimc1lem2  44293  ioodvbdlimc2lem  44295  dvnxpaek  44303  dvnprodlem3  44309  itgioocnicc  44338  ovolsplit  44349  stoweidlem14  44375  stoweidlem55  44416  stoweid  44424  dirkertrigeqlem3  44461  dirkertrigeq  44462  dirkercncf  44468  fourierdlem9  44477  fourierdlem30  44498  fourierdlem31  44499  fourierdlem33  44501  fourierdlem34  44502  fourierdlem35  44503  fourierdlem42  44510  fourierdlem43  44511  fourierdlem46  44513  fourierdlem48  44515  fourierdlem49  44516  fourierdlem51  44518  fourierdlem54  44521  fourierdlem62  44529  fourierdlem64  44531  fourierdlem65  44532  fourierdlem70  44537  fourierdlem71  44538  fourierdlem73  44540  fourierdlem74  44541  fourierdlem75  44542  fourierdlem76  44543  fourierdlem79  44546  fourierdlem81  44548  fourierdlem82  44549  fourierdlem89  44556  fourierdlem91  44558  fourierdlem102  44569  fourierdlem114  44581  sqwvfoura  44589  fourierswlem  44591  fouriersw  44592  elaa2lem  44594  etransclem25  44620  etransclem28  44623  etransclem35  44630  etransclem38  44633  qndenserrnbl  44656  ioorrnopn  44666  ioorrnopnxrlem  44667  ioorrnopnxr  44668  prsal  44679  issalnnd  44706  sge0cl  44742  sge0pr  44755  sge0prle  44762  sge0isum  44788  sge0xaddlem1  44794  iundjiun  44821  meadjun  44823  ismeannd  44828  caragenfiiuncl  44876  caragenunicl  44885  isomennd  44892  hoicvr  44909  ovnssle  44922  ovn0  44927  ovnsubadd  44933  hoidmvval0b  44951  hoidmvlelem2  44957  hoidmvlelem3  44958  hoidmvle  44961  ovnhoilem1  44962  ovnhoi  44964  ovnlecvr2  44971  hoiqssbl  44986  hspmbllem2  44988  hspmbl  44990  vonhoire  45033  iunhoiioo  45037  vonioo  45043  vonicc  45046  vonsn  45052  smfpimltxr  45108  smfpimgtxr  45141  smfrec  45150  fmtnoprmfac1  45877  fmtnoprmfac2  45879  lighneallem3  45919