Theorem neqne 2948

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2940

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 2941

This theorem is referenced by:  exmidne  2950  2f1fvneq  7280  domwdom  9614  epnsym  9649  dfac2b  10171  fin23lem14  10373  axcc2lem  10476  fiminre2  12216  cshw1  14860  xptrrel  15019  dvdsabseq  16350  ncoprmgcdne1b  16687  sgrp2rid2  18939  symg2bas  19410  symgextf  19435  odlem1  19553  gexlem1  19597  ablsimpgfind  20130  psgndiflemB  21618  cply1mul  22300  dmatmul  22503  mdetdiag  22605  mdetunilem9  22626  maducoeval2  22646  madurid  22650  chfacfisf  22860  chfacfisfcpmat  22861  plyexmo  26355  aalioulem3  26376  dvradcnv  26464  logtayllem  26701  logtayl  26702  upgriswlk  29659  lfgrwlkprop  29705  2pthnloop  29751  umgr2adedgspth  29968  umgrclwwlkge2  30010  n4cyclfrgr  30310  frgrwopreglem3  30333  frgrregorufr0  30343  domnmuln0rd  33278  elrspunsn  33457  satfv1lem  35367  bj-rest10b  37090  aks6d1c2p2  42120  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  aks6d1c6lem3  42173  aks6d1c7  42185  unitscyglem2  42197  metakunt2  42207  xppss12  42268  sn-0tie0  42469  prjspnfv01  42634  prjspner01  42635  fiiuncl  45070  disjf1  45188  fzisoeu  45312  fzdifsuc2  45322  supxrge  45349  suplesup  45350  infrpge  45362  xrlexaddrp  45363  infleinflem1  45381  infleinflem2  45382  infleinf  45383  xralrple3  45385  xrralrecnnge  45401  infxrpnf  45457  supminfxr  45475  fsumsupp0  45593  limcresiooub  45657  limcresioolb  45658  limclr  45670  climisp  45761  climxlim2lem  45860  dfxlim2v  45862  xlimliminflimsup  45877  icccncfext  45902  cncfiooiccre  45910  dvbdfbdioolem2  45944  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnxpaek  45957  dvnprodlem3  45963  itgioocnicc  45992  ovolsplit  46003  stoweidlem14  46029  stoweidlem55  46070  stoweid  46078  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkercncf  46122  fourierdlem9  46131  fourierdlem30  46152  fourierdlem31  46153  fourierdlem33  46155  fourierdlem34  46156  fourierdlem35  46157  fourierdlem42  46164  fourierdlem43  46165  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem51  46172  fourierdlem54  46175  fourierdlem62  46183  fourierdlem64  46185  fourierdlem65  46186  fourierdlem70  46191  fourierdlem71  46192  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem79  46200  fourierdlem81  46202  fourierdlem82  46203  fourierdlem89  46210  fourierdlem91  46212  fourierdlem102  46223  fourierdlem114  46235  sqwvfoura  46243  fourierswlem  46245  fouriersw  46246  elaa2lem  46248  etransclem25  46274  etransclem28  46277  etransclem35  46284  etransclem38  46287  qndenserrnbl  46310  ioorrnopn  46320  ioorrnopnxrlem  46321  ioorrnopnxr  46322  prsal  46333  issalnnd  46360  sge0cl  46396  sge0pr  46409  sge0prle  46416  sge0isum  46442  sge0xaddlem1  46448  iundjiun  46475  meadjun  46477  ismeannd  46482  caragenfiiuncl  46530  caragenunicl  46539  isomennd  46546  hoicvr  46563  ovnssle  46576  ovn0  46581  ovnsubadd  46587  hoidmvval0b  46605  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvle  46615  ovnhoilem1  46616  ovnhoi  46618  ovnlecvr2  46625  hoiqssbl  46640  hspmbllem2  46642  hspmbl  46644  vonhoire  46687  iunhoiioo  46691  vonioo  46697  vonicc  46700  vonsn  46706  smfpimltxr  46762  smfpimgtxr  46795  smfrec  46804  fmtnoprmfac1  47552  fmtnoprmfac2  47554  lighneallem3  47594