Theorem neqne 2942

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2934

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 208  df-ne 2935

This theorem is referenced by:  exmidne  2944  domwdom  9479  epnsym  9521  dfac2b  10044  fin23lem14  10246  axcc2lem  10349  fiminre2  12095  cshw1  14775  xptrrel  14933  dvdsabseq  16273  ncoprmgcdne1b  16610  sgrp2rid2  18888  symg2bas  19359  symgextf  19383  odlem1  19501  gexlem1  19545  ablsimpgfind  20078  psgndiflemB  21575  cply1mul  22282  dmatmul  22480  mdetdiag  22582  mdetunilem9  22603  maducoeval2  22623  madurid  22627  chfacfisf  22837  chfacfisfcpmat  22838  plyexmo  26297  aalioulem3  26318  dvradcnv  26404  logtayllem  26641  logtayl  26642  upgriswlk  29727  lfgrwlkprop  29772  2pthnloop  29817  umgr2adedgspth  30034  umgrclwwlkge2  30079  n4cyclfrgr  30379  frgrwopreglem3  30402  frgrregorufr0  30412  domnmuln0rd  33355  elrspunsn  33512  satfv1lem  35590  bj-rest10b  37447  aks6d1c2p2  42604  sticksstones10  42640  sticksstones12a  42642  sticksstones12  42643  aks6d1c6lem3  42657  aks6d1c7  42669  unitscyglem2  42681  xppss12  42716  sn-0tie0  42941  prjspnfv01  43074  prjspner01  43075  fiiuncl  45513  disjf1  45630  fzisoeu  45748  fzdifsuc2  45758  supxrge  45783  suplesup  45784  infrpge  45796  xrlexaddrp  45797  infleinflem1  45814  infleinflem2  45815  infleinf  45816  xralrple3  45818  xrralrecnnge  45834  infxrpnf  45889  supminfxr  45907  fsumsupp0  46023  limcresiooub  46085  limcresioolb  46086  limclr  46098  climisp  46189  climxlim2lem  46288  dfxlim2v  46290  xlimliminflimsup  46305  icccncfext  46330  cncfiooiccre  46338  dvbdfbdioolem2  46372  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnxpaek  46385  dvnprodlem3  46391  itgioocnicc  46420  ovolsplit  46431  stoweidlem14  46457  stoweidlem55  46498  stoweid  46506  dirkertrigeqlem3  46543  dirkertrigeq  46544  dirkercncf  46550  fourierdlem9  46559  fourierdlem30  46580  fourierdlem31  46581  fourierdlem33  46583  fourierdlem34  46584  fourierdlem35  46585  fourierdlem42  46592  fourierdlem43  46593  fourierdlem46  46595  fourierdlem48  46597  fourierdlem49  46598  fourierdlem51  46600  fourierdlem54  46603  fourierdlem62  46611  fourierdlem64  46613  fourierdlem65  46614  fourierdlem70  46619  fourierdlem71  46620  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem76  46625  fourierdlem79  46628  fourierdlem81  46630  fourierdlem82  46631  fourierdlem89  46638  fourierdlem91  46640  fourierdlem102  46651  fourierdlem114  46663  sqwvfoura  46671  fourierswlem  46673  fouriersw  46674  elaa2lem  46676  etransclem25  46702  etransclem28  46705  etransclem35  46712  etransclem38  46715  qndenserrnbl  46738  ioorrnopn  46748  ioorrnopnxrlem  46749  ioorrnopnxr  46750  prsal  46761  issalnnd  46788  sge0cl  46824  sge0pr  46837  sge0prle  46844  sge0isum  46870  sge0xaddlem1  46876  iundjiun  46903  meadjun  46905  ismeannd  46910  caragenfiiuncl  46958  caragenunicl  46967  isomennd  46974  hoicvr  46991  ovnssle  47004  ovn0  47009  ovnsubadd  47015  hoidmvval0b  47033  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvle  47043  ovnhoilem1  47044  ovnhoi  47046  ovnlecvr2  47053  hoiqssbl  47068  hspmbllem2  47070  hspmbl  47072  vonhoire  47115  iunhoiioo  47119  vonioo  47125  vonicc  47128  vonsn  47134  smfpimltxr  47190  smfpimgtxr  47223  smfrec  47232  fmtnoprmfac1  48043  fmtnoprmfac2  48045  lighneallem3  48085  pgn4cyclex  48617