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

Theorem neqne 3024
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 3023 1 𝐴 = 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1533  wne 3016
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 209  df-ne 3017
This theorem is referenced by:  exmidne  3026  2f1fvneq  7012  domwdom  9032  epnsym  9066  dfac2b  9550  fin23lem14  9749  axcc2lem  9852  cshw1  14178  xptrrel  14334  pwm1geoserOLD  15219  dvdsabseq  15657  ncoprmgcdne1b  15988  sgrp2rid2  18085  symg2bas  18515  symgextf  18539  odlem1  18657  gexlem1  18698  ablsimpgfind  19226  cply1mul  20456  psgndiflemB  20738  dmatmul  21100  mdetdiag  21202  mdetunilem9  21223  maducoeval2  21243  madurid  21247  chfacfisf  21456  chfacfisfcpmat  21457  plyexmo  24896  aalioulem3  24917  dvradcnv  25003  logtayllem  25236  logtayl  25237  upgriswlk  27416  lfgrwlkprop  27463  2pthnloop  27506  umgr2adedgspth  27721  umgrclwwlkge2  27763  n4cyclfrgr  28064  frgrwopreglem3  28087  frgrregorufr0  28097  satfv1lem  32604  bj-rest10b  34374  xppss12  39108  fiiuncl  41320  disjf1  41435  fzisoeu  41559  fzdifsuc2  41569  supxrge  41598  suplesup  41599  infrpge  41611  xrlexaddrp  41612  infleinflem1  41630  infleinflem2  41631  infleinf  41632  xralrple3  41634  fiminre2  41638  xrralrecnnge  41654  infxrpnf  41713  supminfxr  41732  fsumsupp0  41851  limcresiooub  41915  limcresioolb  41916  limclr  41928  climisp  42019  climxlim2lem  42118  dfxlim2v  42120  xlimliminflimsup  42135  icccncfext  42162  cncfiooiccre  42170  dvbdfbdioolem2  42206  ioodvbdlimc1lem2  42209  ioodvbdlimc2lem  42211  dvnxpaek  42219  dvnprodlem3  42225  itgioocnicc  42254  ovolsplit  42266  stoweidlem14  42292  stoweidlem55  42333  stoweid  42341  dirkertrigeqlem3  42378  dirkertrigeq  42379  dirkercncf  42385  fourierdlem9  42394  fourierdlem30  42415  fourierdlem31  42416  fourierdlem33  42418  fourierdlem34  42419  fourierdlem35  42420  fourierdlem42  42427  fourierdlem43  42428  fourierdlem46  42430  fourierdlem48  42432  fourierdlem49  42433  fourierdlem51  42435  fourierdlem54  42438  fourierdlem62  42446  fourierdlem64  42448  fourierdlem65  42449  fourierdlem70  42454  fourierdlem71  42455  fourierdlem73  42457  fourierdlem74  42458  fourierdlem75  42459  fourierdlem76  42460  fourierdlem79  42463  fourierdlem81  42465  fourierdlem82  42466  fourierdlem89  42473  fourierdlem91  42475  fourierdlem102  42486  fourierdlem114  42498  sqwvfoura  42506  fourierswlem  42508  fouriersw  42509  elaa2lem  42511  etransclem25  42537  etransclem28  42540  etransclem35  42547  etransclem38  42550  qndenserrnbl  42573  ioorrnopn  42583  ioorrnopnxrlem  42584  ioorrnopnxr  42585  prsal  42596  issalnnd  42621  sge0cl  42656  sge0pr  42669  sge0prle  42676  sge0isum  42702  sge0xaddlem1  42708  iundjiun  42735  meadjun  42737  ismeannd  42742  caragenfiiuncl  42790  caragenunicl  42799  isomennd  42806  hoicvr  42823  ovnssle  42836  ovn0  42841  ovnsubadd  42847  hoidmvval0b  42865  hoidmvlelem2  42871  hoidmvlelem3  42872  hoidmvle  42875  ovnhoilem1  42876  ovnhoi  42878  ovnlecvr2  42885  hoiqssbl  42900  hspmbllem2  42902  hspmbl  42904  vonhoire  42947  iunhoiioo  42951  vonioo  42957  vonicc  42960  vonsn  42966  smfpimltxr  43017  smfpimgtxr  43049  smfrec  43057  fmtnoprmfac1  43720  fmtnoprmfac2  43722  lighneallem3  43765
  Copyright terms: Public domain W3C validator