Theorem neqne 2967

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

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

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 2960

This theorem is used by:  exmidne  2969  domwdom  9605  epnsym  9647  dfac2b  10248  fin23lem14  10450  axcc2lem  10553  fiminre2  12305  cshw1  15015  xptrrel  15176  dvdsabseq  16527  ncoprmgcdne1b  16869  sgrp2rid2  19175  symg2bas  19658  symgextf  19682  odlem1  19800  gexlem1  19844  ablsimpgfind  20377  psgndiflemB  21961  cply1mul  22669  dmatmul  22867  mdetdiag  22969  mdetunilem9  22990  maducoeval2  23010  madurid  23014  chfacfisf  23227  chfacfisfcpmat  23228  plyexmo  26691  aalioulem3  26718  dvradcnv  26805  logtayllem  27044  logtayl  27045  upgriswlk  30278  lfgrwlkprop  30327  2pthnloop  30374  umgr2adedgspth  30594  umgrclwwlkge2  30639  n4cyclfrgr  30949  frgrwopreglem3  30972  frgrregorufr0  30982  domnmuln0rd  33937  elrspunsn  34083  drnglring  34128  dflringlem3  34132  dflring4  34134  satfv1lem  36335  bj-rest10b  38280  aks6d1c2p2  43435  sticksstones10  43471  sticksstones12a  43473  sticksstones12  43474  aks6d1c6lem3  43488  aks6d1c7  43500  unitscyglem2  43512  xppss12  43550  sn-0tie0  43781  fiiuncl  46356  disjf1  46471  fzisoeu  46589  fzdifsuc2  46599  supxrge  46623  suplesup  46624  infrpge  46636  xrlexaddrp  46637  infleinflem1  46654  infleinflem2  46655  infleinf  46656  xralrple3  46658  xrralrecnnge  46674  infxrpnf  46729  supminfxr  46747  fsumsupp0  46863  limcresiooub  46925  limcresioolb  46926  limclr  46938  climisp  47029  climxlim2lem  47128  dfxlim2v  47130  xlimliminflimsup  47145  icccncfext  47170  cncfiooiccre  47178  dvbdfbdioolem2  47212  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvnxpaek  47225  dvnprodlem3  47231  itgioocnicc  47260  ovolsplit  47271  stoweidlem14  47297  stoweidlem55  47338  stoweid  47346  dirkertrigeqlem3  47383  dirkertrigeq  47384  dirkercncf  47390  fourierdlem9  47399  fourierdlem30  47420  fourierdlem31  47421  fourierdlem33  47423  fourierdlem34  47424  fourierdlem35  47425  fourierdlem42  47432  fourierdlem43  47433  fourierdlem46  47435  fourierdlem48  47437  fourierdlem49  47438  fourierdlem51  47440  fourierdlem54  47443  fourierdlem62  47451  fourierdlem64  47453  fourierdlem65  47454  fourierdlem70  47459  fourierdlem71  47460  fourierdlem73  47462  fourierdlem74  47463  fourierdlem75  47464  fourierdlem76  47465  fourierdlem79  47468  fourierdlem81  47470  fourierdlem82  47471  fourierdlem89  47478  fourierdlem91  47480  fourierdlem102  47491  fourierdlem114  47503  sqwvfoura  47511  fourierswlem  47513  fouriersw  47514  elaa2lem  47516  etransclem25  47542  etransclem28  47545  etransclem35  47552  etransclem38  47555  qndenserrnbl  47578  ioorrnopn  47588  ioorrnopnxrlem  47589  ioorrnopnxr  47590  prsal  47601  issalnnd  47628  sge0cl  47664  sge0pr  47677  sge0prle  47684  sge0isum  47710  sge0xaddlem1  47716  iundjiun  47743  meadjun  47745  ismeannd  47750  caragenfiiuncl  47798  caragenunicl  47807  isomennd  47814  hoicvr  47831  ovnssle  47844  ovn0  47849  ovnsubadd  47855  hoidmvval0b  47873  hoidmvlelem2  47879  hoidmvlelem3  47880  hoidmvle  47883  ovnhoilem1  47884  ovnhoi  47886  ovnlecvr2  47893  hoiqssbl  47908  hspmbllem2  47910  hspmbl  47912  vonhoire  47955  iunhoiioo  47959  vonioo  47965  vonicc  47968  vonsn  47974  smfpimltxr  48030  smfpimgtxr  48063  smfrec  48072  fmtnoprmfac1  48923  fmtnoprmfac2  48925  lighneallem3  48965  pgn4cyclex  49497