MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neqne Structured version   Visualization version   GIF version

Theorem neqne 2928
Description: From non equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Assertion
Ref Expression
neqne 𝐴 = 𝐵𝐴𝐵)

Proof of Theorem neqne
StepHypRef Expression
1 id 22 . 2 𝐴 = 𝐵 → ¬ 𝐴 = 𝐵)
21neqned 2927 1 𝐴 = 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1620  wne 2920
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 2921
This theorem is referenced by:  exmidne  2930  epnsym  8665  dfac2b  9114  pwm1geoser  14770  dvdsabseq  15208  symg2bas  17989  upgriswlk  26718  lfgrwlkprop  26765  2pthnloop  26808  umgr2adedgspth  27039  clwwlknclwwlkdifsOLD  27073  umgrclwwlkge2  27085  n4cyclfrgr  27416  frgrwopreglem3  27439  frgrregorufr0  27449  bj-rest10b  33319  fiiuncl  39702  disjxp1  39706  disjf1  39837  fzisoeu  39982  fzdifsuc2  39992  supxrge  40021  suplesup  40022  infrpge  40034  xrlexaddrp  40035  infleinflem1  40053  infleinflem2  40054  infleinf  40055  xralrple3  40057  fiminre2  40061  xrralrecnnge  40080  infxrpnf  40141  supminfxr  40161  fsumsupp0  40282  limcresiooub  40346  limcresioolb  40347  limclr  40359  climisp  40450  climxlim2lem  40543  dfxlim2v  40545  icccncfext  40572  cncfiooiccre  40580  dvbdfbdioolem2  40616  ioodvbdlimc1lem2  40619  ioodvbdlimc2lem  40621  dvnxpaek  40629  dvnprodlem3  40635  itgioocnicc  40665  ovolsplit  40677  stoweidlem14  40703  stoweidlem55  40744  stoweid  40752  dirkertrigeqlem3  40789  dirkertrigeq  40790  dirkercncf  40796  fourierdlem9  40805  fourierdlem30  40826  fourierdlem31  40827  fourierdlem33  40829  fourierdlem34  40830  fourierdlem35  40831  fourierdlem42  40838  fourierdlem43  40839  fourierdlem46  40841  fourierdlem48  40843  fourierdlem49  40844  fourierdlem51  40846  fourierdlem54  40849  fourierdlem62  40857  fourierdlem64  40859  fourierdlem65  40860  fourierdlem70  40865  fourierdlem71  40866  fourierdlem73  40868  fourierdlem74  40869  fourierdlem75  40870  fourierdlem76  40871  fourierdlem79  40874  fourierdlem81  40876  fourierdlem82  40877  fourierdlem89  40884  fourierdlem91  40886  fourierdlem102  40897  fourierdlem114  40909  sqwvfoura  40917  fourierswlem  40919  fouriersw  40920  elaa2lem  40922  etransclem25  40948  etransclem28  40951  etransclem35  40958  etransclem38  40961  qndenserrnbl  40987  ioorrnopn  40997  ioorrnopnxrlem  40998  ioorrnopnxr  40999  prsal  41010  issalnnd  41035  sge0cl  41070  sge0pr  41083  sge0prle  41090  sge0isum  41116  sge0xaddlem1  41122  iundjiun  41149  meadjun  41151  ismeannd  41156  caragenfiiuncl  41204  caragenunicl  41213  isomennd  41220  hoicvr  41237  ovnssle  41250  ovn0  41255  ovnsubadd  41261  hoidmvval0b  41279  hoidmvlelem2  41285  hoidmvlelem3  41286  hoidmvle  41289  ovnhoilem1  41290  ovnhoi  41292  ovnlecvr2  41299  hoiqssbl  41314  hspmbllem2  41316  hspmbl  41318  vonhoire  41361  iunhoiioo  41365  vonioo  41371  vonicc  41374  vonsn  41380  smfpimltxr  41431  smfpimgtxr  41463  smfrec  41471  fmtnoprmfac1  41956  fmtnoprmfac2  41958  lighneallem3  42003
  Copyright terms: Public domain W3C validator