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

Theorem neqne 3021
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 3020 1 𝐴 = 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3013
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 208  df-ne 3014
This theorem is referenced by:  exmidne  3023  2f1fvneq  7009  domwdom  9026  epnsym  9060  dfac2b  9544  fin23lem14  9743  axcc2lem  9846  cshw1  14172  xptrrel  14328  pwm1geoserOLD  15213  dvdsabseq  15651  ncoprmgcdne1b  15982  sgrp2rid2  18029  symg2bas  18455  symgextf  18474  odlem1  18592  gexlem1  18633  ablsimpgfind  19161  cply1mul  20390  psgndiflemB  20672  dmatmul  21034  mdetdiag  21136  mdetunilem9  21157  maducoeval2  21177  madurid  21181  chfacfisf  21390  chfacfisfcpmat  21391  plyexmo  24829  aalioulem3  24850  dvradcnv  24936  logtayllem  25169  logtayl  25170  upgriswlk  27349  lfgrwlkprop  27396  2pthnloop  27439  umgr2adedgspth  27654  umgrclwwlkge2  27696  n4cyclfrgr  27997  frgrwopreglem3  28020  frgrregorufr0  28030  satfv1lem  32506  bj-rest10b  34274  xppss12  38993  fiiuncl  41204  disjf1  41319  fzisoeu  41443  fzdifsuc2  41453  supxrge  41482  suplesup  41483  infrpge  41495  xrlexaddrp  41496  infleinflem1  41514  infleinflem2  41515  infleinf  41516  xralrple3  41518  fiminre2  41522  xrralrecnnge  41538  infxrpnf  41597  supminfxr  41616  fsumsupp0  41735  limcresiooub  41799  limcresioolb  41800  limclr  41812  climisp  41903  climxlim2lem  42002  dfxlim2v  42004  xlimliminflimsup  42019  icccncfext  42046  cncfiooiccre  42054  dvbdfbdioolem2  42090  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  dvnxpaek  42103  dvnprodlem3  42109  itgioocnicc  42138  ovolsplit  42150  stoweidlem14  42176  stoweidlem55  42217  stoweid  42225  dirkertrigeqlem3  42262  dirkertrigeq  42263  dirkercncf  42269  fourierdlem9  42278  fourierdlem30  42299  fourierdlem31  42300  fourierdlem33  42302  fourierdlem34  42303  fourierdlem35  42304  fourierdlem42  42311  fourierdlem43  42312  fourierdlem46  42314  fourierdlem48  42316  fourierdlem49  42317  fourierdlem51  42319  fourierdlem54  42322  fourierdlem62  42330  fourierdlem64  42332  fourierdlem65  42333  fourierdlem70  42338  fourierdlem71  42339  fourierdlem73  42341  fourierdlem74  42342  fourierdlem75  42343  fourierdlem76  42344  fourierdlem79  42347  fourierdlem81  42349  fourierdlem82  42350  fourierdlem89  42357  fourierdlem91  42359  fourierdlem102  42370  fourierdlem114  42382  sqwvfoura  42390  fourierswlem  42392  fouriersw  42393  elaa2lem  42395  etransclem25  42421  etransclem28  42424  etransclem35  42431  etransclem38  42434  qndenserrnbl  42457  ioorrnopn  42467  ioorrnopnxrlem  42468  ioorrnopnxr  42469  prsal  42480  issalnnd  42505  sge0cl  42540  sge0pr  42553  sge0prle  42560  sge0isum  42586  sge0xaddlem1  42592  iundjiun  42619  meadjun  42621  ismeannd  42626  caragenfiiuncl  42674  caragenunicl  42683  isomennd  42690  hoicvr  42707  ovnssle  42720  ovn0  42725  ovnsubadd  42731  hoidmvval0b  42749  hoidmvlelem2  42755  hoidmvlelem3  42756  hoidmvle  42759  ovnhoilem1  42760  ovnhoi  42762  ovnlecvr2  42769  hoiqssbl  42784  hspmbllem2  42786  hspmbl  42788  vonhoire  42831  iunhoiioo  42835  vonioo  42841  vonicc  42844  vonsn  42850  smfpimltxr  42901  smfpimgtxr  42933  smfrec  42941  fmtnoprmfac1  43604  fmtnoprmfac2  43606  lighneallem3  43649
  Copyright terms: Public domain W3C validator