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

Theorem neqne 2651
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
StepHypRef Expression
1 id 22 . 2  |-  ( -.  A  =  B  ->  -.  A  =  B
)
21neqned 2650 1  |-  ( -.  A  =  B  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1452    =/= wne 2641
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 190  df-ne 2643
This theorem is referenced by:  fiiuncl  37465  disjxp1  37470  disjf1  37528  fzisoeu  37606  fzdifsuc2  37618  supxrge  37648  suplesup  37649  infrpge  37661  xrlexaddrp  37662  infleinflem1  37680  infleinflem2  37681  infleinf  37682  fsumsupp0  37753  limcresiooub  37820  limcresioolb  37821  limclr  37833  icccncfext  37862  cncfiooiccre  37870  dvbdfbdioolem2  37898  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  dvnxpaek  37914  dvnprodlem3  37920  itgioocnicc  37951  ovolsplit  37963  stoweidlem14  37986  stoweidlem55  38028  stoweid  38037  dirkertrigeqlem3  38074  dirkertrigeq  38075  dirkercncf  38081  fourierdlem9  38090  fourierdlem30  38111  fourierdlem31  38112  fourierdlem31OLD  38113  fourierdlem33  38115  fourierdlem34  38116  fourierdlem35  38117  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem43  38126  fourierdlem46  38128  fourierdlem48  38130  fourierdlem49  38131  fourierdlem51  38133  fourierdlem54  38136  fourierdlem62  38144  fourierdlem64  38146  fourierdlem65  38147  fourierdlem70  38152  fourierdlem71  38153  fourierdlem73  38155  fourierdlem74  38156  fourierdlem75  38157  fourierdlem76  38158  fourierdlem79  38161  fourierdlem81  38163  fourierdlem82  38164  fourierdlem89  38171  fourierdlem91  38173  fourierdlem102  38184  fourierdlem114  38196  sqwvfoura  38204  fourierswlem  38206  fouriersw  38207  elaa2lem  38209  elaa2lemOLD  38210  etransclem25  38236  etransclem28  38239  etransclem35  38246  etransclem38  38249  qndenserrnbl  38276  prsal  38291  issalnnd  38316  sge0cl  38337  sge0pr  38350  sge0prle  38357  sge0isum  38383  sge0xaddlem1  38389  nnfoctbdjlem  38409  iundjiun  38414  meadjun  38416  ismeannd  38421  caragenfiiuncl  38455  caragenunicl  38464  isomennd  38471  hoicvr  38488  ovnssle  38501  ovn0  38506  ovnsubadd  38512  hoidmvval0b  38530  hoidmvlelem2  38536  hoidmvlelem3  38537  hoidmvle  38540  ovnhoilem1  38541  ovnhoi  38543  ovnlecvr2  38550  hoiqssbl  38565  hspmbllem2  38567  hspmbl  38569  lfgrwlkprop  39879  2pthnloop  39924  umgr2adedgspth  40070
  Copyright terms: Public domain W3C validator