Theorem neqne 2995

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2987

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 210  df-ne 2988

This theorem is referenced by:  exmidne  2997  2f1fvneq  6996  domwdom  9022  epnsym  9056  dfac2b  9541  fin23lem14  9744  axcc2lem  9847  cshw1  14175  xptrrel  14331  pwm1geoserOLD  15217  dvdsabseq  15655  ncoprmgcdne1b  15984  sgrp2rid2  18083  symg2bas  18513  symgextf  18537  odlem1  18655  gexlem1  18696  ablsimpgfind  19225  psgndiflemB  20289  cply1mul  20923  dmatmul  21102  mdetdiag  21204  mdetunilem9  21225  maducoeval2  21245  madurid  21249  chfacfisf  21459  chfacfisfcpmat  21460  plyexmo  24909  aalioulem3  24930  dvradcnv  25016  logtayllem  25250  logtayl  25251  upgriswlk  27430  lfgrwlkprop  27477  2pthnloop  27520  umgr2adedgspth  27734  umgrclwwlkge2  27776  n4cyclfrgr  28076  frgrwopreglem3  28099  frgrregorufr0  28109  satfv1lem  32722  bj-rest10b  34504  metakunt2  39351  xppss12  39409  sn-0tie0  39576  fiiuncl  41699  disjf1  41809  fzisoeu  41932  fzdifsuc2  41942  supxrge  41970  suplesup  41971  infrpge  41983  xrlexaddrp  41984  infleinflem1  42002  infleinflem2  42003  infleinf  42004  xralrple3  42006  fiminre2  42010  xrralrecnnge  42026  infxrpnf  42084  supminfxr  42103  fsumsupp0  42220  limcresiooub  42284  limcresioolb  42285  limclr  42297  climisp  42388  climxlim2lem  42487  dfxlim2v  42489  xlimliminflimsup  42504  icccncfext  42529  cncfiooiccre  42537  dvbdfbdioolem2  42571  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvnxpaek  42584  dvnprodlem3  42590  itgioocnicc  42619  ovolsplit  42630  stoweidlem14  42656  stoweidlem55  42697  stoweid  42705  dirkertrigeqlem3  42742  dirkertrigeq  42743  dirkercncf  42749  fourierdlem9  42758  fourierdlem30  42779  fourierdlem31  42780  fourierdlem33  42782  fourierdlem34  42783  fourierdlem35  42784  fourierdlem42  42791  fourierdlem43  42792  fourierdlem46  42794  fourierdlem48  42796  fourierdlem49  42797  fourierdlem51  42799  fourierdlem54  42802  fourierdlem62  42810  fourierdlem64  42812  fourierdlem65  42813  fourierdlem70  42818  fourierdlem71  42819  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem79  42827  fourierdlem81  42829  fourierdlem82  42830  fourierdlem89  42837  fourierdlem91  42839  fourierdlem102  42850  fourierdlem114  42862  sqwvfoura  42870  fourierswlem  42872  fouriersw  42873  elaa2lem  42875  etransclem25  42901  etransclem28  42904  etransclem35  42911  etransclem38  42914  qndenserrnbl  42937  ioorrnopn  42947  ioorrnopnxrlem  42948  ioorrnopnxr  42949  prsal  42960  issalnnd  42985  sge0cl  43020  sge0pr  43033  sge0prle  43040  sge0isum  43066  sge0xaddlem1  43072  iundjiun  43099  meadjun  43101  ismeannd  43106  caragenfiiuncl  43154  caragenunicl  43163  isomennd  43170  hoicvr  43187  ovnssle  43200  ovn0  43205  ovnsubadd  43211  hoidmvval0b  43229  hoidmvlelem2  43235  hoidmvlelem3  43236  hoidmvle  43239  ovnhoilem1  43240  ovnhoi  43242  ovnlecvr2  43249  hoiqssbl  43264  hspmbllem2  43266  hspmbl  43268  vonhoire  43311  iunhoiioo  43315  vonioo  43321  vonicc  43324  vonsn  43330  smfpimltxr  43381  smfpimgtxr  43413  smfrec  43421  fmtnoprmfac1  44082  fmtnoprmfac2  44084  lighneallem3  44125