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

Theorem neeq1d 3049
Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
Hypothesis
Ref Expression
neeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
neeq1d (𝜑 → (𝐴𝐶𝐵𝐶))

Proof of Theorem neeq1d
StepHypRef Expression
1 neeq1d.1 . . 3 (𝜑𝐴 = 𝐵)
21eqeq1d 2803 . 2 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐶))
32necon3bid 3034 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wne 2990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-ne 2991
This theorem is referenced by:  neeq1  3052  eqnetrd  3057  inisegn0  5932  f12dfv  7012  f13dfv  7013  suppval1  7823  elsuppfn  7825  suppsnop  7831  ressuppss  7836  ressuppssdif  7838  tz7.49  8068  ereldm  8324  pw2f1olem  8608  marypha1lem  8885  wdomtr  9027  inf3lem2  9080  cantnflem1  9140  cantnf  9144  cplem2  9307  dfac9  9551  kmlem12  9576  infpssrlem4  9721  fin23lem14  9748  axcc2lem  9851  axcc3  9853  domtriomlem  9857  axdc2lem  9863  ac6c4  9896  zorn2lem6  9916  rpnnen1lem4  12371  rpnnen1lem5  12372  mptnn0fsuppr  13366  hashprg  13756  hashtpg  13843  prodfn0  15246  prodfrec  15247  prodfdiv  15248  ntrivcvgtail  15252  fproddiv  15311  fprodn0  15329  fproddivf  15337  dvdsle  15656  algcvg  15914  algcvga  15917  eucalgcvga  15924  rpdvds  15998  phibndlem  16101  dfphi2  16105  pcaddlem  16218  vdwmc  16308  iscatd2  16948  brcic  17064  cicer  17072  sgrp2nmndlem5  18090  symgextf1lem  18544  pmtrmvd  18580  frgpup3lem  18899  isirred  19449  isdrngrd  19525  rrgsupp  20061  dsmmelbas  20432  dsmmacl  20434  frlmssuvc2  20488  elcls  21682  clsndisj  21684  elcls3  21692  neindisj2  21732  clslp  21757  cmpfi  22017  cmpfii  22018  dfconn2  22028  connsuba  22029  nconnsubb  22032  1stcelcls  22070  finlocfin  22129  locfincmp  22135  dissnlocfin  22138  locfindis  22139  ptclsg  22224  dfac14lem  22226  isfbas  22438  trfbas2  22452  isfil  22456  filss  22462  fbunfip  22478  fgval  22479  elfg  22480  isufil2  22517  ufileu  22528  filufint  22529  fmfnfm  22567  flimclslem  22593  fclsopni  22624  fclsnei  22628  fclsbas  22630  fclsrest  22633  fclscmp  22639  ufilcmp  22641  isfcf  22643  fcfnei  22644  fcfneii  22646  ptcmplem2  22662  cnextcn  22676  cnextfres1  22677  tsmsfbas  22737  iscusp  22909  cuspcvg  22911  lpbl  23114  prdsxmslem2  23140  restmetu  23181  qdensere  23379  lebnumlem3  23572  isphtpc  23603  iscmet  23892  cmetcvg  23893  equivcmet  23925  cmetcusp1  23961  cmetcusp  23962  rrxmvallem  24012  ovolicc2lem2  24126  ovolicc2lem5  24129  i1fres  24313  lhop1lem  24620  deg1ldg  24697  plyco0  24793  plyeq0lem  24811  coeeq2  24843  coe1termlem  24859  taylfval  24958  cxpeq0  25273  ftalem4  25665  ftalem5  25666  ftalem6  25667  isppw  25703  isnsqf  25724  sqff1o  25771  musum  25780  dchrelbas3  25826  dchrelbasd  25827  dchrelbas4  25831  dchrmulcl  25837  dchrn0  25838  dchrfi  25843  dchrptlem2  25853  dchrpt  25855  lgsne0  25923  lgsdchr  25943  2sqlem11  26017  ishlg  26400  uvtx01vtx  27191  pthdlem2lem  27560  2pthdlem1  27720  clwwlknclwwlkdif  27768  umgr2cwwkdifex  27854  3pthdlem1  27953  frgrregorufr  28114  numclwwlk2lem1lem  28131  numclwwlk2lem1  28165  numclwlk2lem2f  28166  numclwlk2lem2f1o  28168  nmorepnf  28555  nmoprepnf  29654  nmfnrepnf  29667  ressupprn  30454  disjdsct  30466  rmfsupp2  30921  isufd  31075  fedgmullem2  31118  locfinreflem  31197  sibfof  31712  signswch  31945  signstfvneq0  31956  derangenlem  32532  subfacp1lem3  32543  subfacp1lem5  32545  subfacp1lem6  32546  subfacp1  32547  iscvm  32620  cvmcov  32624  cvmcov2  32636  eldm3  33111  elima4  33133  nosupbnd2lem1  33329  neibastop1  33821  neibastop2lem  33822  neibastop2  33823  neibastop3  33824  neifg  33833  poimirlem17  35073  poimirlem18  35074  poimirlem20  35076  poimirlem21  35077  poimirlem22  35078  poimirlem23  35079  poimirlem27  35083  poimirlem28  35084  poimirlem30  35086  poimirlem31  35087  poimirlem32  35088  mblfinlem3  35095  itg2addnclem3  35109  sstotbnd2  35211  cntotbnd  35233  heibor1lem  35246  dmecd  35721  br1cosscnvxrn  35873  2llnm3N  36864  dalem4  36960  cdlemk28-3  38203  mapdh9a  39084  metakunt29  39375  fsuppind  39453  dffltz  39612  pellexlem3  39769  mncn0  40080  aaitgo  40103  gneispace0nelrn2  40841  cvgdvgrat  41014  binomcxplemnotnn0  41057  disjf1  41806  disjrnmpt2  41812  disjinfi  41817  fsumiunss  42214  islptre  42258  islpcn  42278  lptre2pt  42279  0ellimcdiv  42288  liminflelimsup  42415  stoweidlem28  42667  stoweidlem43  42682  dirkercncflem2  42743  fourierdlem46  42791  fourierdlem79  42824  elaa2lem  42872  elaa2  42873  sge0fodjrnlem  43052  sge0iunmpt  43054  nnfoctbdjlem  43091  meadjiunlem  43101  meadjiun  43102  ovn0ssdmfun  44384  nzerooringczr  44693  rmsupp0  44767  scmsuppss  44771  suppmptcfin  44778  linc1  44831  el0ldep  44872  ldepspr  44879  islindeps2  44889  zlmodzxzldeplem4  44909  zlmodzxzldep  44910  ldepsnlinclem1  44911  ldepsnlinclem2  44912  ldepsnlinc  44914  secval  45270  cscval  45271  cotval  45272
  Copyright terms: Public domain W3C validator