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

Theorem neeq1d 3004
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 2739 . 2 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐶))
32necon3bid 2989 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wne 2944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-ne 2945
This theorem is referenced by:  neeq1  3007  eqnetrd  3012  inisegn0  6055  f12dfv  7224  f13dfv  7225  suppval1  8103  elsuppfng  8106  elsuppfn  8107  suppsnop  8114  ressuppss  8119  ressuppssdif  8121  tz7.49  8396  ereldm  8703  pw2f1olem  9027  marypha1lem  9376  wdomtr  9518  inf3lem2  9572  cantnflem1  9632  cantnf  9636  cplem2  9833  dfac9  10079  kmlem12  10104  infpssrlem4  10249  fin23lem14  10276  axcc2lem  10379  axcc3  10381  domtriomlem  10385  axdc2lem  10391  ac6c4  10424  zorn2lem6  10444  rpnnen1lem4  12912  rpnnen1lem5  12913  mptnn0fsuppr  13911  hashprg  14302  hashtpg  14391  prodfn0  15786  prodfrec  15787  prodfdiv  15788  ntrivcvgtail  15792  fproddiv  15851  fprodn0  15869  fproddivf  15877  dvdsle  16199  algcvg  16459  algcvga  16462  eucalgcvga  16469  rpdvds  16543  phibndlem  16649  dfphi2  16653  pcaddlem  16767  vdwmc  16857  iscatd2  17568  brcic  17688  cicer  17696  cat1lem  17989  cat1  17990  sgrp2nmndlem5  18746  symgextf1lem  19209  pmtrmvd  19245  frgpup3lem  19566  isirred  20137  isdrngrd  20229  isdrngrdOLD  20231  rrgsupp  20777  dsmmelbas  21161  dsmmacl  21163  frlmssuvc2  21217  mhpsclcl  21553  mhpmulcl  21555  elcls  22440  clsndisj  22442  elcls3  22450  neindisj2  22490  clslp  22515  cmpfi  22775  cmpfii  22776  dfconn2  22786  connsuba  22787  nconnsubb  22790  1stcelcls  22828  finlocfin  22887  locfincmp  22893  dissnlocfin  22896  locfindis  22897  ptclsg  22982  dfac14lem  22984  isfbas  23196  trfbas2  23210  isfil  23214  filss  23220  fbunfip  23236  fgval  23237  elfg  23238  isufil2  23275  ufileu  23286  filufint  23287  fmfnfm  23325  flimclslem  23351  fclsopni  23382  fclsnei  23386  fclsbas  23388  fclsrest  23391  fclscmp  23397  ufilcmp  23399  isfcf  23401  fcfnei  23402  fcfneii  23404  ptcmplem2  23420  cnextcn  23434  cnextfres1  23435  tsmsfbas  23495  iscusp  23667  cuspcvg  23669  lpbl  23875  prdsxmslem2  23901  restmetu  23942  qdensere  24149  lebnumlem3  24342  isphtpc  24373  iscmet  24664  cmetcvg  24665  equivcmet  24697  cmetcusp1  24733  cmetcusp  24734  rrxmvallem  24784  ovolicc2lem2  24898  ovolicc2lem5  24901  i1fres  25086  lhop1lem  25393  deg1ldg  25473  plyco0  25569  plyeq0lem  25587  coeeq2  25619  coe1termlem  25635  taylfval  25734  cxpeq0  26049  ftalem4  26441  ftalem5  26442  ftalem6  26443  isppw  26479  isnsqf  26500  sqff1o  26547  musum  26556  dchrelbas3  26602  dchrelbasd  26603  dchrelbas4  26607  dchrmulcl  26613  dchrn0  26614  dchrfi  26619  dchrptlem2  26629  dchrpt  26631  lgsne0  26699  lgsdchr  26719  2sqlem11  26793  nosupbnd2lem1  27079  ishlg  27586  uvtx01vtx  28387  pthdlem2lem  28757  2pthdlem1  28917  clwwlknclwwlkdif  28965  umgr2cwwkdifex  29051  3pthdlem1  29150  frgrregorufr  29311  numclwwlk2lem1lem  29328  numclwwlk2lem1  29362  numclwlk2lem2f  29363  numclwlk2lem2f1o  29365  nmorepnf  29752  nmoprepnf  30851  nmfnrepnf  30864  ressupprn  31647  disjdsct  31658  rmfsupp2  32115  isufd  32300  fedgmullem2  32365  locfinreflem  32461  sibfof  32980  signswch  33213  signstfvneq0  33224  derangenlem  33805  subfacp1lem3  33816  subfacp1lem5  33818  subfacp1lem6  33819  subfacp1  33820  iscvm  33893  cvmcov  33897  cvmcov2  33909  eldm3  34373  elima4  34389  neibastop1  34860  neibastop2lem  34861  neibastop2  34862  neibastop3  34863  neifg  34872  poimirlem17  36124  poimirlem18  36125  poimirlem20  36127  poimirlem21  36128  poimirlem22  36129  poimirlem23  36130  poimirlem27  36134  poimirlem28  36135  poimirlem30  36137  poimirlem31  36138  poimirlem32  36139  mblfinlem3  36146  itg2addnclem3  36160  sstotbnd2  36262  cntotbnd  36284  heibor1lem  36297  dmecd  36794  disjecxrn  36880  br1cosscnvxrn  36965  2llnm3N  38061  dalem4  38157  cdlemk28-3  39400  mapdh9a  40281  sticksstones1  40583  metakunt29  40634  fsuppind  40794  dffltz  41001  pellexlem3  41183  mncn0  41495  aaitgo  41518  gneispace0nelrn2  42487  cvgdvgrat  42667  binomcxplemnotnn0  42710  disjf1  43475  disjrnmpt2  43481  disjinfi  43486  fsumiunss  43890  islptre  43934  islpcn  43954  lptre2pt  43955  0ellimcdiv  43964  liminflelimsup  44091  stoweidlem28  44343  stoweidlem43  44358  dirkercncflem2  44419  fourierdlem46  44467  fourierdlem79  44500  elaa2lem  44548  elaa2  44549  sge0fodjrnlem  44731  sge0iunmpt  44733  nnfoctbdjlem  44770  meadjiunlem  44780  meadjiun  44781  ovn0ssdmfun  46135  nzerooringczr  46444  rmsupp0  46518  scmsuppss  46522  suppmptcfin  46529  linc1  46580  el0ldep  46621  ldepspr  46628  islindeps2  46638  zlmodzxzldeplem4  46658  zlmodzxzldep  46659  ldepsnlinclem1  46660  ldepsnlinclem2  46661  ldepsnlinc  46663  fvconstr  46996  fvconstrn0  46997  fvconstr2  46998  catprslem  47104  catprsc  47107  catprsc2  47108  secval  47266  cscval  47267  cotval  47268
  Copyright terms: Public domain W3C validator