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

Theorem neeq1d 3072
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 2820 . 2 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐶))
32necon3bid 3057 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wne 3013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-ne 3014
This theorem is referenced by:  neeq1  3075  eqnetrd  3080  inisegn0  5954  f12dfv  7021  f13dfv  7022  suppval1  7825  elsuppfn  7827  suppsnop  7833  ressuppss  7838  ressuppssdif  7840  tz7.49  8070  ereldm  8326  pw2f1olem  8609  marypha1lem  8885  wdomtr  9027  inf3lem2  9080  cantnflem1  9140  cantnf  9144  cplem2  9307  dfac9  9550  kmlem12  9575  infpssrlem4  9716  fin23lem14  9743  axcc2lem  9846  axcc3  9848  domtriomlem  9852  axdc2lem  9858  ac6c4  9891  zorn2lem6  9911  rpnnen1lem4  12367  rpnnen1lem5  12368  mptnn0fsuppr  13355  hashprg  13744  hashtpg  13831  prodfn0  15238  prodfrec  15239  prodfdiv  15240  ntrivcvgtail  15244  fproddiv  15303  fprodn0  15321  fproddivf  15329  dvdsle  15648  algcvg  15908  algcvga  15911  eucalgcvga  15918  rpdvds  15992  phibndlem  16095  dfphi2  16099  pcaddlem  16212  vdwmc  16302  iscatd2  16940  brcic  17056  cicer  17064  sgrp2nmndlem5  18032  symgextf1lem  18477  pmtrmvd  18513  frgpup3lem  18832  isirred  19378  isdrngrd  19457  rrgsupp  19992  dsmmelbas  20811  dsmmacl  20813  frlmssuvc2  20867  elcls  21609  clsndisj  21611  elcls3  21619  neindisj2  21659  clslp  21684  cmpfi  21944  cmpfii  21945  dfconn2  21955  connsuba  21956  nconnsubb  21959  1stcelcls  21997  finlocfin  22056  locfincmp  22062  dissnlocfin  22065  locfindis  22066  ptclsg  22151  dfac14lem  22153  isfbas  22365  trfbas2  22379  isfil  22383  filss  22389  fbunfip  22405  fgval  22406  elfg  22407  isufil2  22444  ufileu  22455  filufint  22456  fmfnfm  22494  flimclslem  22520  fclsopni  22551  fclsnei  22555  fclsbas  22557  fclsrest  22560  fclscmp  22566  ufilcmp  22568  isfcf  22570  fcfnei  22571  fcfneii  22573  ptcmplem2  22589  cnextcn  22603  cnextfres1  22604  tsmsfbas  22663  iscusp  22835  cuspcvg  22837  lpbl  23040  prdsxmslem2  23066  restmetu  23107  qdensere  23305  lebnumlem3  23494  isphtpc  23525  iscmet  23814  cmetcvg  23815  equivcmet  23847  cmetcusp1  23883  cmetcusp  23884  rrxmvallem  23934  ovolicc2lem2  24046  ovolicc2lem5  24049  i1fres  24233  lhop1lem  24537  deg1ldg  24613  plyco0  24709  plyeq0lem  24727  coeeq2  24759  coe1termlem  24775  taylfval  24874  cxpeq0  25188  ftalem4  25580  ftalem5  25581  ftalem6  25582  isppw  25618  isnsqf  25639  sqff1o  25686  musum  25695  dchrelbas3  25741  dchrelbasd  25742  dchrelbas4  25746  dchrmulcl  25752  dchrn0  25753  dchrfi  25758  dchrptlem2  25768  dchrpt  25770  lgsne0  25838  lgsdchr  25858  2sqlem11  25932  ishlg  26315  uvtx01vtx  27106  pthdlem2lem  27475  2pthdlem1  27636  clwwlknclwwlkdif  27684  umgr2cwwkdifex  27771  3pthdlem1  27870  frgrregorufr  28031  numclwwlk2lem1lem  28048  numclwwlk2lem1  28082  numclwlk2lem2f  28083  numclwlk2lem2f1o  28085  nmorepnf  28472  nmoprepnf  29571  nmfnrepnf  29584  disjdsct  30364  rmfsupp2  30793  fedgmullem2  30925  locfinreflem  31003  sibfof  31497  signswch  31730  signstfvneq0  31741  derangenlem  32315  subfacp1lem3  32326  subfacp1lem5  32328  subfacp1lem6  32329  subfacp1  32330  iscvm  32403  cvmcov  32407  cvmcov2  32419  eldm3  32894  elima4  32916  nosupbnd2lem1  33112  neibastop1  33604  neibastop2lem  33605  neibastop2  33606  neibastop3  33607  neifg  33616  poimirlem17  34790  poimirlem18  34791  poimirlem20  34793  poimirlem21  34794  poimirlem22  34795  poimirlem23  34796  poimirlem27  34800  poimirlem28  34801  poimirlem30  34803  poimirlem31  34804  poimirlem32  34805  mblfinlem3  34812  itg2addnclem3  34826  sstotbnd2  34933  cntotbnd  34955  heibor1lem  34968  dmecd  35443  br1cosscnvxrn  35594  2llnm3N  36585  dalem4  36681  cdlemk28-3  37924  mapdh9a  38805  dffltz  39149  pellexlem3  39306  mncn0  39617  aaitgo  39640  gneispace0nelrn2  40369  cvgdvgrat  40522  binomcxplemnotnn0  40565  disjf1  41319  disjrnmpt2  41325  disjinfi  41330  fsumiunss  41732  islptre  41776  islpcn  41796  lptre2pt  41797  0ellimcdiv  41806  liminflelimsup  41933  stoweidlem28  42190  stoweidlem43  42205  dirkercncflem2  42266  fourierdlem46  42314  fourierdlem79  42347  elaa2lem  42395  elaa2  42396  sge0fodjrnlem  42575  sge0iunmpt  42577  nnfoctbdjlem  42614  meadjiunlem  42624  meadjiun  42625  ovn0ssdmfun  43911  nzerooringczr  44271  rmsupp0  44344  scmsuppss  44348  suppmptcfin  44355  linc1  44408  el0ldep  44449  ldepspr  44456  islindeps2  44466  zlmodzxzldeplem4  44486  zlmodzxzldep  44487  ldepsnlinclem1  44488  ldepsnlinclem2  44489  ldepsnlinc  44491  secval  44774  cscval  44775  cotval  44776
  Copyright terms: Public domain W3C validator