Theorem neqne 2933

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  exmidne  2935  domwdom  9503  epnsym  9538  dfac2b  10060  fin23lem14  10262  axcc2lem  10365  fiminre2  12107  cshw1  14763  xptrrel  14922  dvdsabseq  16259  ncoprmgcdne1b  16596  sgrp2rid2  18829  symg2bas  19299  symgextf  19323  odlem1  19441  gexlem1  19485  ablsimpgfind  20018  psgndiflemB  21485  cply1mul  22159  dmatmul  22360  mdetdiag  22462  mdetunilem9  22483  maducoeval2  22503  madurid  22507  chfacfisf  22717  chfacfisfcpmat  22718  plyexmo  26197  aalioulem3  26218  dvradcnv  26306  logtayllem  26544  logtayl  26545  upgriswlk  29544  lfgrwlkprop  29589  2pthnloop  29634  umgr2adedgspth  29851  umgrclwwlkge2  29893  n4cyclfrgr  30193  frgrwopreglem3  30216  frgrregorufr0  30226  domnmuln0rd  33198  elrspunsn  33373  satfv1lem  35322  bj-rest10b  37050  aks6d1c2p2  42080  sticksstones10  42116  sticksstones12a  42118  sticksstones12  42119  aks6d1c6lem3  42133  aks6d1c7  42145  unitscyglem2  42157  xppss12  42190  sn-0tie0  42412  prjspnfv01  42585  prjspner01  42586  fiiuncl  45032  disjf1  45150  fzisoeu  45271  fzdifsuc2  45281  supxrge  45307  suplesup  45308  infrpge  45320  xrlexaddrp  45321  infleinflem1  45339  infleinflem2  45340  infleinf  45341  xralrple3  45343  xrralrecnnge  45359  infxrpnf  45415  supminfxr  45433  fsumsupp0  45549  limcresiooub  45613  limcresioolb  45614  limclr  45626  climisp  45717  climxlim2lem  45816  dfxlim2v  45818  xlimliminflimsup  45833  icccncfext  45858  cncfiooiccre  45866  dvbdfbdioolem2  45900  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  dvnxpaek  45913  dvnprodlem3  45919  itgioocnicc  45948  ovolsplit  45959  stoweidlem14  45985  stoweidlem55  46026  stoweid  46034  dirkertrigeqlem3  46071  dirkertrigeq  46072  dirkercncf  46078  fourierdlem9  46087  fourierdlem30  46108  fourierdlem31  46109  fourierdlem33  46111  fourierdlem34  46112  fourierdlem35  46113  fourierdlem42  46120  fourierdlem43  46121  fourierdlem46  46123  fourierdlem48  46125  fourierdlem49  46126  fourierdlem51  46128  fourierdlem54  46131  fourierdlem62  46139  fourierdlem64  46141  fourierdlem65  46142  fourierdlem70  46147  fourierdlem71  46148  fourierdlem73  46150  fourierdlem74  46151  fourierdlem75  46152  fourierdlem76  46153  fourierdlem79  46156  fourierdlem81  46158  fourierdlem82  46159  fourierdlem89  46166  fourierdlem91  46168  fourierdlem102  46179  fourierdlem114  46191  sqwvfoura  46199  fourierswlem  46201  fouriersw  46202  elaa2lem  46204  etransclem25  46230  etransclem28  46233  etransclem35  46240  etransclem38  46243  qndenserrnbl  46266  ioorrnopn  46276  ioorrnopnxrlem  46277  ioorrnopnxr  46278  prsal  46289  issalnnd  46316  sge0cl  46352  sge0pr  46365  sge0prle  46372  sge0isum  46398  sge0xaddlem1  46404  iundjiun  46431  meadjun  46433  ismeannd  46438  caragenfiiuncl  46486  caragenunicl  46495  isomennd  46502  hoicvr  46519  ovnssle  46532  ovn0  46537  ovnsubadd  46543  hoidmvval0b  46561  hoidmvlelem2  46567  hoidmvlelem3  46568  hoidmvle  46571  ovnhoilem1  46572  ovnhoi  46574  ovnlecvr2  46581  hoiqssbl  46596  hspmbllem2  46598  hspmbl  46600  vonhoire  46643  iunhoiioo  46647  vonioo  46653  vonicc  46656  vonsn  46662  smfpimltxr  46718  smfpimgtxr  46751  smfrec  46760  fmtnoprmfac1  47539  fmtnoprmfac2  47541  lighneallem3  47581  pgn4cyclex  48089