Theorem neqne 2945

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ≠ wne 2937

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 2938

This theorem is referenced by:  exmidne  2947  2f1fvneq  7279  domwdom  9611  epnsym  9646  dfac2b  10168  fin23lem14  10370  axcc2lem  10473  fiminre2  12213  cshw1  14856  xptrrel  15015  dvdsabseq  16346  ncoprmgcdne1b  16683  sgrp2rid2  18951  symg2bas  19424  symgextf  19449  odlem1  19567  gexlem1  19611  ablsimpgfind  20144  psgndiflemB  21635  cply1mul  22315  dmatmul  22518  mdetdiag  22620  mdetunilem9  22641  maducoeval2  22661  madurid  22665  chfacfisf  22875  chfacfisfcpmat  22876  plyexmo  26369  aalioulem3  26390  dvradcnv  26478  logtayllem  26715  logtayl  26716  upgriswlk  29673  lfgrwlkprop  29719  2pthnloop  29763  umgr2adedgspth  29977  umgrclwwlkge2  30019  n4cyclfrgr  30319  frgrwopreglem3  30342  frgrregorufr0  30352  domnmuln0rd  33260  elrspunsn  33436  satfv1lem  35346  bj-rest10b  37071  aks6d1c2p2  42100  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  aks6d1c6lem3  42153  aks6d1c7  42165  unitscyglem2  42177  metakunt2  42187  xppss12  42246  sn-0tie0  42445  prjspnfv01  42610  prjspner01  42611  fiiuncl  45004  disjf1  45125  fzisoeu  45250  fzdifsuc2  45260  supxrge  45287  suplesup  45288  infrpge  45300  xrlexaddrp  45301  infleinflem1  45319  infleinflem2  45320  infleinf  45321  xralrple3  45323  xrralrecnnge  45339  infxrpnf  45395  supminfxr  45413  fsumsupp0  45533  limcresiooub  45597  limcresioolb  45598  limclr  45610  climisp  45701  climxlim2lem  45800  dfxlim2v  45802  xlimliminflimsup  45817  icccncfext  45842  cncfiooiccre  45850  dvbdfbdioolem2  45884  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnxpaek  45897  dvnprodlem3  45903  itgioocnicc  45932  ovolsplit  45943  stoweidlem14  45969  stoweidlem55  46010  stoweid  46018  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkercncf  46062  fourierdlem9  46071  fourierdlem30  46092  fourierdlem31  46093  fourierdlem33  46095  fourierdlem34  46096  fourierdlem35  46097  fourierdlem42  46104  fourierdlem43  46105  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem51  46112  fourierdlem54  46115  fourierdlem62  46123  fourierdlem64  46125  fourierdlem65  46126  fourierdlem70  46131  fourierdlem71  46132  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem79  46140  fourierdlem81  46142  fourierdlem82  46143  fourierdlem89  46150  fourierdlem91  46152  fourierdlem102  46163  fourierdlem114  46175  sqwvfoura  46183  fourierswlem  46185  fouriersw  46186  elaa2lem  46188  etransclem25  46214  etransclem28  46217  etransclem35  46224  etransclem38  46227  qndenserrnbl  46250  ioorrnopn  46260  ioorrnopnxrlem  46261  ioorrnopnxr  46262  prsal  46273  issalnnd  46300  sge0cl  46336  sge0pr  46349  sge0prle  46356  sge0isum  46382  sge0xaddlem1  46388  iundjiun  46415  meadjun  46417  ismeannd  46422  caragenfiiuncl  46470  caragenunicl  46479  isomennd  46486  hoicvr  46503  ovnssle  46516  ovn0  46521  ovnsubadd  46527  hoidmvval0b  46545  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvle  46555  ovnhoilem1  46556  ovnhoi  46558  ovnlecvr2  46565  hoiqssbl  46580  hspmbllem2  46582  hspmbl  46584  vonhoire  46627  iunhoiioo  46631  vonioo  46637  vonicc  46640  vonsn  46646  smfpimltxr  46702  smfpimgtxr  46735  smfrec  46744  fmtnoprmfac1  47489  fmtnoprmfac2  47491  lighneallem3  47531