Theorem neeq1d 2702

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 2425	. 2 |- ( ph -> ( A = C <-> B = C ) )
3	2	necon3bid 2683	1 |- ( ph -> ( A =/= C <-> B =/= C ) )

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1438   =/= wne 2619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-cleq 2415  df-ne 2621

This theorem is referenced by:  neeq12dOLD  2705  neeq1  2706  eqnetrd  2718  prnzg  4118  inisegn0  5217  f12dfv  6185  f13dfv  6186  suppval1  6929  elsuppfn  6931  suppsnop  6937  ressuppss  6943  ressuppssdif  6945  tz7.49  7168  ereldm  7413  pw2f1olem  7680  marypha1lem  7951  wdomtr  8094  inf3lem2  8138  cantnflem1  8197  cantnf  8201  cplem2  8364  dfac9  8568  kmlem12  8593  infpssrlem4  8738  fin23lem14  8765  axcc2lem  8868  axcc3  8870  domtriomlem  8874  axdc2lem  8880  ac6c4  8913  zorn2lem6  8933  rpnnen1lem4  11295  rpnnen1lem5  11296  mptnn0fsuppr  12212  hashprg  12573  hashtpg  12639  prodfn0  13943  prodfrec  13944  prodfdiv  13945  ntrivcvgtail  13949  fproddiv  14008  fprodn0  14026  fproddivf  14034  dvdsle  14343  algcvg  14528  algcvga  14531  eucalgcvga  14538  rpdvds  14669  phibndlem  14711  dfphi2  14715  pcaddlem  14826  vdwmc  14921  iscatd2  15580  brcic  15696  cicer  15704  sgrp2nmndlem5  16656  symgextf1lem  17054  pmtrmvd  17090  frgpup3lem  17420  isirred  17920  isdrngrd  17994  rrgsupp  18508  dsmmelbas  19294  dsmmacl  19296  frlmssuvc2  19345  elcls  20081  clsndisj  20083  elcls3  20091  neindisj2  20131  clslp  20156  cmpfi  20415  cmpfii  20416  dfcon2  20426  consuba  20427  nconsubb  20430  1stcelcls  20468  finlocfin  20527  locfincmp  20533  dissnlocfin  20536  locfindis  20537  ptclsg  20622  dfac14lem  20624  isfbas  20836  trfbas2  20850  isfil  20854  filss  20860  fbunfip  20876  fgval  20877  elfg  20878  isufil2  20915  ufileu  20926  filufint  20927  fmfnfm  20965  flimclslem  20991  fclsopni  21022  fclsnei  21026  fclsbas  21028  fclsrest  21031  fclscmp  21037  ufilcmp  21039  isfcf  21041  fcfnei  21042  fcfneii  21044  ptcmplem2  21060  cnextcn  21074  cnextfres1  21075  tsmsfbas  21134  iscusp  21306  cuspcvg  21308  lpbl  21510  prdsxmslem2  21536  restmetu  21577  qdensere  21782  lebnumlem3  21983  lebnumlem3OLD  21986  isphtpc  22017  iscmet  22246  cmetcvg  22247  equivcmet  22277  cmetcusp1  22312  cmetcusp  22313  rrxmvallem  22350  ovolicc2lem2  22463  ovolicc2lem5  22467  i1fres  22655  lhop1lem  22957  deg1ldg  23033  plyco0  23138  plyeq0lem  23156  coeeq2  23188  coe1termlem  23204  taylfval  23306  cxpeq0  23615  ftalem4  23992  ftalem5  23993  ftalem4OLD  23994  ftalem5OLD  23995  ftalem6  23996  isppw  24033  isnsqf  24054  sqff1o  24101  musum  24112  dchrelbas3  24158  dchrelbasd  24159  dchrelbas4  24163  dchrmulcl  24169  dchrn0  24170  dchrfi  24175  dchrptlem2  24185  dchrpt  24187  lgsne0  24253  lgsdchr  24268  2sqlem11  24295  ishlg  24639  uvtx01vtx  25212  usg2cwwkdifex  25541  frgraregorufr  25773  clwwlkextfrlem1  25796  numclwwlkovh  25821  numclwwlk2lem1  25822  numclwlk2lem2f  25823  numclwlk2lem2f1o  25825  numclwwlk5  25832  nmorepnf  26401  nmoprepnf  27512  nmfnrepnf  27525  disjdsct  28279  locfinreflem  28669  sibfof  29175  signswch  29452  signstfvneq0  29463  derangenlem  29896  subfacp1lem3  29907  subfacp1lem5  29909  subfacp1lem6  29910  subfacp1  29911  iscvm  29984  cvmcov  29988  cvmcov2  30000  eldm3  30403  elima4  30422  nobndlem2  30581  nobndlem4  30583  nobndlem5  30584  nobndlem6  30585  nobndlem8  30587  nobndup  30588  nobnddown  30589  nofulllem5  30594  neibastop1  31014  neibastop2lem  31015  neibastop2  31016  neibastop3  31017  neifg  31026  poimirlem17  31877  poimirlem18  31878  poimirlem20  31880  poimirlem21  31881  poimirlem22  31882  poimirlem23  31883  poimirlem27  31887  poimirlem28  31888  poimirlem30  31890  poimirlem31  31891  poimirlem32  31892  mblfinlem3  31899  itg2addnclem3  31915  sstotbnd2  32026  cntotbnd  32048  heibor1lem  32061  2llnm3N  33059  dalem4  33155  cdlemk28-3  34400  mapdh9a  35283  pellexlem3  35601  mncn0  35924  aaitgo  35954  cvgdvgrat  36526  binomcxplemnotnn0  36569  disjf1  37313  disjrnmpt2  37319  disjinfi  37324  fsumiunss  37483  islptre  37525  islpcn  37545  lptre2pt  37546  0ellimcdiv  37556  stoweidlem28  37714  stoweidlem43  37730  dirkercncflem2  37792  fourierdlem46  37842  fourierdlem79  37875  elaa2lem  37923  elaa2lemOLD  37924  elaa2  37925  sge0fodjrnlem  38052  sge0iunmpt  38054  nnfoctbdjlem  38078  meadjiunlem  38088  meadjiun  38089  ovn0ssdmfun  39071  nzerooringczr  39378  rmsupp0  39459  scmsuppss  39463  suppmptcfin  39470  linc1  39524  el0ldep  39565  ldepspr  39572  islindeps2  39582  zlmodzxzldeplem4  39602  zlmodzxzldep  39603  ldepsnlinclem1  39604  ldepsnlinclem2  39605  ldepsnlinc  39607  secval  39773  cscval  39774  cotval  39775