Theorem neeq1d 2718

Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Hypothesis

Ref	Expression
neeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
neeq1d	|- ( ph -> ( A =/= C <-> B =/= C ) )

Proof of Theorem neeq1d

Step	Hyp	Ref	Expression
1		neeq1d.1	. . 3 |- ( ph -> A = B )
2	1	eqeq1d 2443	. 2 |- ( ph -> ( A = C <-> B = C ) )
3	2	necon3bid 2699	1 |- ( ph -> ( A =/= C <-> B =/= C ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1381   =/= wne 2636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-cleq 2433  df-ne 2638

This theorem is referenced by:  neeq12dOLD  2721  neeq1  2722  eqnetrd  2734  prnzg  4131  f12dfv  6160  f13dfv  6161  suppval1  6905  elsuppfn  6907  suppsnop  6913  ressuppss  6917  ressuppssdif  6919  tz7.49  7108  ereldm  7353  pw2f1olem  7619  marypha1lem  7891  wdomtr  7999  inf3lem2  8044  cantnflem1  8106  cantnf  8110  cantnfOLD  8132  cplem2  8306  dfac9  8514  kmlem12  8539  infpssrlem4  8684  fin23lem14  8711  axcc2lem  8814  axcc3  8816  domtriomlem  8820  axdc2lem  8826  ac6c4  8859  zorn2lem6  8879  rpnnen1lem4  11215  rpnnen1lem5  11216  mptnn0fsuppr  12079  hashprg  12434  hashtpg  12497  dvdsle  13903  algcvg  14077  algcvga  14080  eucalgcvga  14087  rpdvds  14137  phibndlem  14172  dfphi2  14176  pcaddlem  14279  vdwmc  14368  iscatd2  14950  sgrp2nmndlem5  15916  symgextf1lem  16314  pmtrmvd  16350  frgpup3lem  16664  isirred  17216  isdrngrd  17290  rrgsupp  17807  dsmmelbas  18637  dsmmacl  18639  frlmssuvc2  18693  frlmssuvc2OLD  18695  elcls  19440  clsndisj  19442  elcls3  19450  neindisj2  19490  clslp  19515  cmpfi  19774  cmpfii  19775  dfcon2  19786  consuba  19787  nconsubb  19790  1stcelcls  19828  finlocfin  19887  locfincmp  19893  dissnlocfin  19896  locfindis  19897  ptclsg  19982  dfac14lem  19984  isfbas  20196  trfbas2  20210  isfil  20214  filss  20220  fbunfip  20236  fgval  20237  elfg  20238  isufil2  20275  ufileu  20286  filufint  20287  fmfnfm  20325  flimclslem  20351  fclsopni  20382  fclsnei  20386  fclsbas  20388  fclsrest  20391  fclscmp  20397  ufilcmp  20399  isfcf  20401  fcfnei  20402  fcfneii  20404  ptcmplem2  20419  cnextcn  20433  cnextfres  20434  tsmsfbas  20492  iscusp  20668  cuspcvg  20670  lpbl  20872  prdsxmslem2  20898  restmetu  20956  qdensere  21143  lebnumlem3  21329  isphtpc  21360  iscmet  21589  cmetcvg  21590  equivcmet  21620  cmetcusp1OLD  21657  cmetcusp1  21658  cmetcuspOLD  21659  cmetcusp  21660  rrxmvallem  21697  ovolicc2lem2  21795  ovolicc2lem5  21798  i1fres  21978  lhop1lem  22280  deg1ldg  22358  plyco0  22455  plyeq0lem  22473  coeeq2  22505  coe1termlem  22520  taylfval  22619  cxpeq0  22924  ftalem4  23214  ftalem5  23215  ftalem6  23216  isppw  23253  isnsqf  23274  sqff1o  23321  musum  23332  dchrelbas3  23378  dchrelbasd  23379  dchrelbas4  23383  dchrmulcl  23389  dchrn0  23390  dchrfi  23395  dchrptlem2  23405  dchrpt  23407  lgsne0  23473  lgsdchr  23488  2sqlem11  23515  ishlg  23851  uvtx01vtx  24357  usg2cwwkdifex  24686  frgraregorufr  24918  clwwlkextfrlem1  24941  numclwwlkovh  24966  numclwwlk2lem1  24967  numclwlk2lem2f  24968  numclwlk2lem2f1o  24970  numclwwlk5  24977  nmorepnf  25548  nmoprepnf  26651  nmfnrepnf  26664  disjdsct  27386  locfinreflem  27709  sibfof  28148  signswch  28384  signstfvneq0  28395  derangenlem  28481  subfacp1lem3  28492  subfacp1lem5  28494  subfacp1lem6  28495  subfacp1  28496  iscvm  28570  cvmcov  28574  cvmcov2  28586  prodfn0  28996  prodfrec  28997  prodfdiv  28998  ntrivcvgtail  29002  fproddiv  29059  fprodn0  29077  eldm3  29159  elima4  29177  nobndlem2  29421  nobndlem4  29423  nobndlem5  29424  nobndlem6  29425  nobndlem8  29427  nobndup  29428  nobnddown  29429  nofulllem5  29434  mblfinlem3  30021  itg2addnclem3  30036  neibastop1  30145  neibastop2lem  30146  neibastop2  30147  neibastop3  30148  neifg  30157  sstotbnd2  30238  cntotbnd  30260  heibor1lem  30273  pellexlem3  30735  inisegn0  30957  mncn0  31057  aaitgo  31080  cvgdvgrat  31163  islptre  31529  islpcn  31549  lptre2pt  31550  0ellimcdiv  31559  stoweidlem28  31695  stoweidlem43  31710  dirkercncflem2  31771  fourierdlem46  31820  fourierdlem79  31853  ovn0ssdmfun  32289  rmsupp0  32671  scmsuppss  32675  suppmptcfin  32682  linc1  32736  el0ldep  32777  ldepspr  32784  islindeps2  32794  zlmodzxzldeplem4  32814  zlmodzxzldep  32815  ldepsnlinclem1  32816  ldepsnlinclem2  32817  ldepsnlinc  32819  secval  32851  cscval  32852  cotval  32853  2llnm3N  34995  dalem4  35091  cdlemk28-3  36336  mapdh9a  37219