Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  neqne Structured version   Visualization version   Unicode version

Theorem neqne 37374
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 2631 1  |-  ( -.  A  =  B  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1444    =/= wne 2622
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 189  df-ne 2624
This theorem is referenced by:  fiiuncl  37406  disjxp1  37411  disjf1  37457  fzisoeu  37518  fzdifsuc2  37530  supxrge  37561  suplesup  37562  infrpge  37574  xrlexaddrp  37575  fsumsupp0  37657  limcresiooub  37723  limcresioolb  37724  limclr  37736  icccncfext  37765  cncfiooiccre  37773  dvbdfbdioolem2  37801  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  dvnxpaek  37817  dvnprodlem3  37823  itgioocnicc  37854  stoweidlem14  37874  stoweidlem55  37916  stoweid  37925  dirkertrigeqlem3  37962  dirkertrigeq  37963  dirkercncf  37969  fourierdlem9  37978  fourierdlem30  37999  fourierdlem31  38000  fourierdlem31OLD  38001  fourierdlem33  38003  fourierdlem34  38004  fourierdlem35  38005  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem43  38014  fourierdlem46  38016  fourierdlem48  38018  fourierdlem49  38019  fourierdlem51  38021  fourierdlem54  38024  fourierdlem62  38032  fourierdlem64  38034  fourierdlem65  38035  fourierdlem70  38040  fourierdlem71  38041  fourierdlem73  38043  fourierdlem74  38044  fourierdlem75  38045  fourierdlem76  38046  fourierdlem79  38049  fourierdlem81  38051  fourierdlem82  38052  fourierdlem89  38059  fourierdlem91  38061  fourierdlem102  38072  fourierdlem114  38084  sqwvfoura  38092  fourierswlem  38094  fouriersw  38095  elaa2lem  38097  elaa2lemOLD  38098  etransclem25  38124  etransclem28  38127  etransclem35  38134  etransclem38  38137  qndenserrnbl  38164  prsal  38179  sge0cl  38223  sge0pr  38236  sge0prle  38243  sge0isum  38269  sge0xaddlem1  38275  nnfoctbdjlem  38293  iundjiun  38298  meadjun  38300  ismeannd  38305  caragenfiiuncl  38336  caragenunicl  38345  isomennd  38352  hoicvr  38370  ovnssle  38383  ovn0  38388  ovnsubadd  38394  hoidmvval0b  38412  hoidmvlelem2  38418  hoidmvlelem3  38419  hoidmvle  38422  ovnhoilem1  38423  ovnhoi  38425  ovnlecvr2  38432  hoiqssbl  38447  hspmbllem2  38449  hspmbl  38451
  Copyright terms: Public domain W3C validator