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

Theorem neqne 2831
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 2830 1 𝐴 = 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wne 2823
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 2824
This theorem is referenced by:  exmidne  2833  pwm1geoser  14644  dvdsabseq  15082  upgriswlk  26593  lfgrwlkprop  26640  2pthnloop  26683  umgr2adedgspth  26913  clwwlknclwwlkdifsOLD  26947  umgrclwwlkge2  26957  n4cyclfrgr  27271  frgrwopreglem3  27294  frgrregorufr0  27304  bj-rest10b  33167  fiiuncl  39548  disjxp1  39552  disjf1  39683  fzisoeu  39828  fzdifsuc2  39838  supxrge  39867  suplesup  39868  infrpge  39880  xrlexaddrp  39881  infleinflem1  39899  infleinflem2  39900  infleinf  39901  xralrple3  39903  fiminre2  39907  xrralrecnnge  39926  infxrpnf  39987  supminfxr  40007  fsumsupp0  40128  limcresiooub  40192  limcresioolb  40193  limclr  40205  climisp  40296  climxlim2lem  40389  dfxlim2v  40391  icccncfext  40418  cncfiooiccre  40426  dvbdfbdioolem2  40462  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnxpaek  40475  dvnprodlem3  40481  itgioocnicc  40511  ovolsplit  40523  stoweidlem14  40549  stoweidlem55  40590  stoweid  40598  dirkertrigeqlem3  40635  dirkertrigeq  40636  dirkercncf  40642  fourierdlem9  40651  fourierdlem30  40672  fourierdlem31  40673  fourierdlem33  40675  fourierdlem34  40676  fourierdlem35  40677  fourierdlem42  40684  fourierdlem43  40685  fourierdlem46  40687  fourierdlem48  40689  fourierdlem49  40690  fourierdlem51  40692  fourierdlem54  40695  fourierdlem62  40703  fourierdlem64  40705  fourierdlem65  40706  fourierdlem70  40711  fourierdlem71  40712  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem79  40720  fourierdlem81  40722  fourierdlem82  40723  fourierdlem89  40730  fourierdlem91  40732  fourierdlem102  40743  fourierdlem114  40755  sqwvfoura  40763  fourierswlem  40765  fouriersw  40766  elaa2lem  40768  etransclem25  40794  etransclem28  40797  etransclem35  40804  etransclem38  40807  qndenserrnbl  40833  ioorrnopn  40843  ioorrnopnxrlem  40844  ioorrnopnxr  40845  prsal  40856  issalnnd  40881  sge0cl  40916  sge0pr  40929  sge0prle  40936  sge0isum  40962  sge0xaddlem1  40968  iundjiun  40995  meadjun  40997  ismeannd  41002  caragenfiiuncl  41050  caragenunicl  41059  isomennd  41066  hoicvr  41083  ovnssle  41096  ovn0  41101  ovnsubadd  41107  hoidmvval0b  41125  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvle  41135  ovnhoilem1  41136  ovnhoi  41138  ovnlecvr2  41145  hoiqssbl  41160  hspmbllem2  41162  hspmbl  41164  vonhoire  41207  iunhoiioo  41211  vonioo  41217  vonicc  41220  vonsn  41226  smfpimltxr  41277  smfpimgtxr  41309  smfrec  41317  fmtnoprmfac1  41802  fmtnoprmfac2  41804  lighneallem3  41849
  Copyright terms: Public domain W3C validator