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

Theorem neeq1d 2882
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 2653 . 2 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐶))
32necon3bid 2867 1 (𝜑 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wne 2823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824
This theorem is referenced by:  neeq1  2885  eqnetrd  2890  prnzgOLD  4343  inisegn0  5532  f12dfv  6569  f13dfv  6570  suppval1  7346  elsuppfn  7348  suppsnop  7354  ressuppss  7359  ressuppssdif  7361  tz7.49  7585  ereldm  7833  pw2f1olem  8105  marypha1lem  8380  wdomtr  8521  inf3lem2  8564  cantnflem1  8624  cantnf  8628  cplem2  8791  dfac9  8996  kmlem12  9021  infpssrlem4  9166  fin23lem14  9193  axcc2lem  9296  axcc3  9298  domtriomlem  9302  axdc2lem  9308  ac6c4  9341  zorn2lem6  9361  rpnnen1lem4  11855  rpnnen1lem5  11856  rpnnen1lem4OLD  11861  rpnnen1lem5OLD  11862  mptnn0fsuppr  12839  hashprg  13220  hashprgOLD  13221  hashtpg  13305  prodfn0  14670  prodfrec  14671  prodfdiv  14672  ntrivcvgtail  14676  fproddiv  14735  fprodn0  14753  fproddivf  14762  dvdsle  15079  algcvg  15336  algcvga  15339  eucalgcvga  15346  rpdvds  15421  phibndlem  15522  dfphi2  15526  pcaddlem  15639  vdwmc  15729  iscatd2  16389  brcic  16505  cicer  16513  sgrp2nmndlem5  17463  symgextf1lem  17886  pmtrmvd  17922  frgpup3lem  18236  isirred  18745  isdrngrd  18821  rrgsupp  19339  dsmmelbas  20131  dsmmacl  20133  frlmssuvc2  20182  elcls  20925  clsndisj  20927  elcls3  20935  neindisj2  20975  clslp  21000  cmpfi  21259  cmpfii  21260  dfconn2  21270  connsuba  21271  nconnsubb  21274  1stcelcls  21312  finlocfin  21371  locfincmp  21377  dissnlocfin  21380  locfindis  21381  ptclsg  21466  dfac14lem  21468  isfbas  21680  trfbas2  21694  isfil  21698  filss  21704  fbunfip  21720  fgval  21721  elfg  21722  isufil2  21759  ufileu  21770  filufint  21771  fmfnfm  21809  flimclslem  21835  fclsopni  21866  fclsnei  21870  fclsbas  21872  fclsrest  21875  fclscmp  21881  ufilcmp  21883  isfcf  21885  fcfnei  21886  fcfneii  21888  ptcmplem2  21904  cnextcn  21918  cnextfres1  21919  tsmsfbas  21978  iscusp  22150  cuspcvg  22152  lpbl  22355  prdsxmslem2  22381  restmetu  22422  qdensere  22620  lebnumlem3  22809  isphtpc  22840  iscmet  23128  cmetcvg  23129  equivcmet  23160  cmetcusp1  23195  cmetcusp  23196  rrxmvallem  23233  ovolicc2lem2  23332  ovolicc2lem5  23335  i1fres  23517  lhop1lem  23821  deg1ldg  23897  plyco0  23993  plyeq0lem  24011  coeeq2  24043  coe1termlem  24059  taylfval  24158  cxpeq0  24469  ftalem4  24847  ftalem5  24848  ftalem6  24849  isppw  24885  isnsqf  24906  sqff1o  24953  musum  24962  dchrelbas3  25008  dchrelbasd  25009  dchrelbas4  25013  dchrmulcl  25019  dchrn0  25020  dchrfi  25025  dchrptlem2  25035  dchrpt  25037  lgsne0  25105  lgsdchr  25125  2sqlem11  25199  ishlg  25542  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  pthdlem2lem  26719  2pthdlem1  26895  clwwlknclwwlkdif  26945  umgr2cwwkdifex  27029  clwlksfclwwlk  27049  3pthdlem1  27142  frgrregorufr  27305  numclwwlk2lem1lem  27324  numclwwlk2lem1lemOLD  27325  numclwwlk2lem1  27356  numclwlk2lem2f  27357  numclwlk2lem2f1o  27359  numclwwlkovhOLD  27362  numclwwlk2lem1OLD  27363  numclwlk2lem2fOLD  27364  numclwlk2lem2f1oOLD  27366  nmorepnf  27751  nmoprepnf  28854  nmfnrepnf  28867  disjdsct  29608  locfinreflem  30035  sibfof  30530  signswch  30766  signstfvneq0  30777  derangenlem  31279  subfacp1lem3  31290  subfacp1lem5  31292  subfacp1lem6  31293  subfacp1  31294  iscvm  31367  cvmcov  31371  cvmcov2  31383  eldm3  31777  elima4  31803  nosupbnd2lem1  31986  neibastop1  32479  neibastop2lem  32480  neibastop2  32481  neibastop3  32482  neifg  32491  poimirlem17  33556  poimirlem18  33557  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem23  33562  poimirlem27  33566  poimirlem28  33567  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  mblfinlem3  33578  itg2addnclem3  33593  sstotbnd2  33703  cntotbnd  33725  heibor1lem  33738  dmecd  34215  br1cosscnvxrn  34364  2llnm3N  35173  dalem4  35269  cdlemk28-3  36513  mapdh9a  37396  pellexlem3  37712  mncn0  38026  aaitgo  38049  gneispace0nelrn2  38756  cvgdvgrat  38829  binomcxplemnotnn0  38872  disjf1  39683  disjrnmpt2  39689  disjinfi  39694  fsumiunss  40125  islptre  40169  islpcn  40189  lptre2pt  40190  0ellimcdiv  40199  liminflelimsup  40326  stoweidlem28  40563  stoweidlem43  40578  dirkercncflem2  40639  fourierdlem46  40687  fourierdlem79  40720  elaa2lem  40768  elaa2  40769  sge0fodjrnlem  40951  sge0iunmpt  40953  nnfoctbdjlem  40990  meadjiunlem  41000  meadjiun  41001  ovn0ssdmfun  42092  nzerooringczr  42397  rmsupp0  42474  scmsuppss  42478  suppmptcfin  42485  linc1  42539  el0ldep  42580  ldepspr  42587  islindeps2  42597  zlmodzxzldeplem4  42617  zlmodzxzldep  42618  ldepsnlinclem1  42619  ldepsnlinclem2  42620  ldepsnlinc  42622  secval  42816  cscval  42817  cotval  42818
  Copyright terms: Public domain W3C validator