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  9485  epnsym  9524  dfac2b  10044  fin23lem14  10246  axcc2lem  10349  fiminre2  12092  cshw1  14747  xptrrel  14906  dvdsabseq  16243  ncoprmgcdne1b  16580  sgrp2rid2  18819  symg2bas  19291  symgextf  19315  odlem1  19433  gexlem1  19477  ablsimpgfind  20010  psgndiflemB  21526  cply1mul  22200  dmatmul  22401  mdetdiag  22503  mdetunilem9  22524  maducoeval2  22544  madurid  22548  chfacfisf  22758  chfacfisfcpmat  22759  plyexmo  26238  aalioulem3  26259  dvradcnv  26347  logtayllem  26585  logtayl  26586  upgriswlk  29605  lfgrwlkprop  29650  2pthnloop  29695  umgr2adedgspth  29912  umgrclwwlkge2  29954  n4cyclfrgr  30254  frgrwopreglem3  30277  frgrregorufr0  30287  domnmuln0rd  33233  elrspunsn  33385  satfv1lem  35354  bj-rest10b  37082  aks6d1c2p2  42112  sticksstones10  42148  sticksstones12a  42150  sticksstones12  42151  aks6d1c6lem3  42165  aks6d1c7  42177  unitscyglem2  42189  xppss12  42222  sn-0tie0  42444  prjspnfv01  42617  prjspner01  42618  fiiuncl  45063  disjf1  45181  fzisoeu  45302  fzdifsuc2  45312  supxrge  45338  suplesup  45339  infrpge  45351  xrlexaddrp  45352  infleinflem1  45369  infleinflem2  45370  infleinf  45371  xralrple3  45373  xrralrecnnge  45389  infxrpnf  45445  supminfxr  45463  fsumsupp0  45579  limcresiooub  45643  limcresioolb  45644  limclr  45656  climisp  45747  climxlim2lem  45846  dfxlim2v  45848  xlimliminflimsup  45863  icccncfext  45888  cncfiooiccre  45896  dvbdfbdioolem2  45930  ioodvbdlimc1lem2  45933  ioodvbdlimc2lem  45935  dvnxpaek  45943  dvnprodlem3  45949  itgioocnicc  45978  ovolsplit  45989  stoweidlem14  46015  stoweidlem55  46056  stoweid  46064  dirkertrigeqlem3  46101  dirkertrigeq  46102  dirkercncf  46108  fourierdlem9  46117  fourierdlem30  46138  fourierdlem31  46139  fourierdlem33  46141  fourierdlem34  46142  fourierdlem35  46143  fourierdlem42  46150  fourierdlem43  46151  fourierdlem46  46153  fourierdlem48  46155  fourierdlem49  46156  fourierdlem51  46158  fourierdlem54  46161  fourierdlem62  46169  fourierdlem64  46171  fourierdlem65  46172  fourierdlem70  46177  fourierdlem71  46178  fourierdlem73  46180  fourierdlem74  46181  fourierdlem75  46182  fourierdlem76  46183  fourierdlem79  46186  fourierdlem81  46188  fourierdlem82  46189  fourierdlem89  46196  fourierdlem91  46198  fourierdlem102  46209  fourierdlem114  46221  sqwvfoura  46229  fourierswlem  46231  fouriersw  46232  elaa2lem  46234  etransclem25  46260  etransclem28  46263  etransclem35  46270  etransclem38  46273  qndenserrnbl  46296  ioorrnopn  46306  ioorrnopnxrlem  46307  ioorrnopnxr  46308  prsal  46319  issalnnd  46346  sge0cl  46382  sge0pr  46395  sge0prle  46402  sge0isum  46428  sge0xaddlem1  46434  iundjiun  46461  meadjun  46463  ismeannd  46468  caragenfiiuncl  46516  caragenunicl  46525  isomennd  46532  hoicvr  46549  ovnssle  46562  ovn0  46567  ovnsubadd  46573  hoidmvval0b  46591  hoidmvlelem2  46597  hoidmvlelem3  46598  hoidmvle  46601  ovnhoilem1  46602  ovnhoi  46604  ovnlecvr2  46611  hoiqssbl  46626  hspmbllem2  46628  hspmbl  46630  vonhoire  46673  iunhoiioo  46677  vonioo  46683  vonicc  46686  vonsn  46692  smfpimltxr  46748  smfpimgtxr  46781  smfrec  46790  fmtnoprmfac1  47569  fmtnoprmfac2  47571  lighneallem3  47611  pgn4cyclex  48130