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

Theorem neqne 2804
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 2803 1 𝐴 = 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1480  wne 2796
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 2797
This theorem is referenced by:  exmidne  2806  pwm1geoser  14520  dvdsabseq  14954  upgriswlk  26400  lfgrwlkprop  26447  2pthnloop  26490  umgr2adedgspth  26707  clwwlknclwwlkdifs  26734  umgrclwwlksge2  26772  n4cyclfrgr  27013  frgrwopreglem3  27035  frgrregorufr0  27041  bj-rest10b  32671  fiiuncl  38705  disjxp1  38709  disjf1  38829  fzisoeu  38965  fzdifsuc2  38976  supxrge  39005  suplesup  39006  infrpge  39018  xrlexaddrp  39019  infleinflem1  39037  infleinflem2  39038  infleinf  39039  xralrple3  39041  fiminre2  39045  xrralrecnnge  39064  fsumsupp0  39201  limcresiooub  39265  limcresioolb  39266  limclr  39278  icccncfext  39391  cncfiooiccre  39399  dvbdfbdioolem2  39437  ioodvbdlimc1lem2  39440  ioodvbdlimc2lem  39442  dvnxpaek  39450  dvnprodlem3  39456  itgioocnicc  39487  ovolsplit  39499  stoweidlem14  39525  stoweidlem55  39566  stoweid  39574  dirkertrigeqlem3  39611  dirkertrigeq  39612  dirkercncf  39618  fourierdlem9  39627  fourierdlem30  39648  fourierdlem31  39649  fourierdlem33  39651  fourierdlem34  39652  fourierdlem35  39653  fourierdlem42  39660  fourierdlem43  39661  fourierdlem46  39663  fourierdlem48  39665  fourierdlem49  39666  fourierdlem51  39668  fourierdlem54  39671  fourierdlem62  39679  fourierdlem64  39681  fourierdlem65  39682  fourierdlem70  39687  fourierdlem71  39688  fourierdlem73  39690  fourierdlem74  39691  fourierdlem75  39692  fourierdlem76  39693  fourierdlem79  39696  fourierdlem81  39698  fourierdlem82  39699  fourierdlem89  39706  fourierdlem91  39708  fourierdlem102  39719  fourierdlem114  39731  sqwvfoura  39739  fourierswlem  39741  fouriersw  39742  elaa2lem  39744  etransclem25  39770  etransclem28  39773  etransclem35  39780  etransclem38  39783  qndenserrnbl  39809  ioorrnopn  39819  ioorrnopnxrlem  39820  ioorrnopnxr  39821  prsal  39832  issalnnd  39857  sge0cl  39892  sge0pr  39905  sge0prle  39912  sge0isum  39938  sge0xaddlem1  39944  iundjiun  39971  meadjun  39973  ismeannd  39978  caragenfiiuncl  40023  caragenunicl  40032  isomennd  40039  hoicvr  40056  ovnssle  40069  ovn0  40074  ovnsubadd  40080  hoidmvval0b  40098  hoidmvlelem2  40104  hoidmvlelem3  40105  hoidmvle  40108  ovnhoilem1  40109  ovnhoi  40111  ovnlecvr2  40118  hoiqssbl  40133  hspmbllem2  40135  hspmbl  40137  vonhoire  40180  iunhoiioo  40184  vonioo  40190  vonicc  40193  vonsn  40199  smfpimltxr  40250  smfpimgtxr  40282  smfrec  40290  fmtnoprmfac1  40764  fmtnoprmfac2  40766  lighneallem3  40811
  Copyright terms: Public domain W3C validator