Theorem neqne 2802

Description: From non equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
neqne	|- ( -. A = B -> A =/= B )

Proof of Theorem neqne

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( -. A = B -> -. A = B )
2	1	neqned 2801	1 |- ( -. A = B -> A =/= B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   =/= wne 2794

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 197  df-ne 2795

This theorem is referenced by:  exmidne  2804  pwm1geoser  14600  dvdsabseq  15035  upgriswlk  26537  lfgrwlkprop  26584  2pthnloop  26627  umgr2adedgspth  26844  clwwlknclwwlkdifs  26873  umgrclwwlksge2  26912  n4cyclfrgr  27155  frgrwopreglem3  27178  frgrregorufr0  27188  bj-rest10b  33042  fiiuncl  39234  disjxp1  39238  disjf1  39369  fzisoeu  39514  fzdifsuc2  39525  supxrge  39554  suplesup  39555  infrpge  39567  xrlexaddrp  39568  infleinflem1  39586  infleinflem2  39587  infleinf  39588  xralrple3  39590  fiminre2  39594  xrralrecnnge  39613  infxrpnf  39674  supminfxr  39694  fsumsupp0  39810  limcresiooub  39874  limcresioolb  39875  limclr  39887  climisp  39978  climxlim2lem  40071  dfxlim2v  40073  icccncfext  40100  cncfiooiccre  40108  dvbdfbdioolem2  40144  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnxpaek  40157  dvnprodlem3  40163  itgioocnicc  40193  ovolsplit  40205  stoweidlem14  40231  stoweidlem55  40272  stoweid  40280  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkercncf  40324  fourierdlem9  40333  fourierdlem30  40354  fourierdlem31  40355  fourierdlem33  40357  fourierdlem34  40358  fourierdlem35  40359  fourierdlem42  40366  fourierdlem43  40367  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem51  40374  fourierdlem54  40377  fourierdlem62  40385  fourierdlem64  40387  fourierdlem65  40388  fourierdlem70  40393  fourierdlem71  40394  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem79  40402  fourierdlem81  40404  fourierdlem82  40405  fourierdlem89  40412  fourierdlem91  40414  fourierdlem102  40425  fourierdlem114  40437  sqwvfoura  40445  fourierswlem  40447  fouriersw  40448  elaa2lem  40450  etransclem25  40476  etransclem28  40479  etransclem35  40486  etransclem38  40489  qndenserrnbl  40515  ioorrnopn  40525  ioorrnopnxrlem  40526  ioorrnopnxr  40527  prsal  40538  issalnnd  40563  sge0cl  40598  sge0pr  40611  sge0prle  40618  sge0isum  40644  sge0xaddlem1  40650  iundjiun  40677  meadjun  40679  ismeannd  40684  caragenfiiuncl  40729  caragenunicl  40738  isomennd  40745  hoicvr  40762  ovnssle  40775  ovn0  40780  ovnsubadd  40786  hoidmvval0b  40804  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvle  40814  ovnhoilem1  40815  ovnhoi  40817  ovnlecvr2  40824  hoiqssbl  40839  hspmbllem2  40841  hspmbl  40843  vonhoire  40886  iunhoiioo  40890  vonioo  40896  vonicc  40899  vonsn  40905  smfpimltxr  40956  smfpimgtxr  40988  smfrec  40996  fmtnoprmfac1  41477  fmtnoprmfac2  41479  lighneallem3  41524