Theorem neeq1d 2728

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1370   =/= wne 2647

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

This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-ne 2649

This theorem is referenced by:  neeq12dOLD  2731  neeq1  2732  eqnetrd  2744  prnzg  4102  suppval1  6805  elsuppfn  6807  suppsnop  6813  ressuppss  6817  ressuppssdif  6819  tz7.49  7009  ereldm  7253  pw2f1olem  7524  marypha1lem  7793  wdomtr  7900  inf3lem2  7945  cantnflem1  8007  cantnf  8011  cantnfOLD  8033  cplem2  8207  dfac9  8415  kmlem12  8440  infpssrlem4  8585  fin23lem14  8612  axcc2lem  8715  axcc3  8717  domtriomlem  8721  axdc2lem  8727  ac6c4  8760  zorn2lem6  8780  rpnnen1lem4  11092  rpnnen1lem5  11093  hashprg  12272  hashtpg  12303  dvdsle  13695  algcvg  13868  algcvga  13871  eucalgcvga  13878  rpdvds  13927  phibndlem  13962  dfphi2  13966  pcaddlem  14067  vdwmc  14156  iscatd2  14737  symgextf1lem  16043  pmtrmvd  16080  frgpup3lem  16394  isirred  16913  isdrngrd  16980  rrgsupp  17484  dsmmelbas  18288  dsmmacl  18290  frlmssuvc2  18344  frlmssuvc2OLD  18346  elcls  18808  clsndisj  18810  elcls3  18818  neindisj2  18858  clslp  18883  cmpfi  19142  cmpfii  19143  dfcon2  19154  consuba  19155  nconsubb  19158  1stcelcls  19196  ptclsg  19319  dfac14lem  19321  isfbas  19533  trfbas2  19547  isfil  19551  filss  19557  fbunfip  19573  fgval  19574  elfg  19575  isufil2  19612  ufileu  19623  filufint  19624  fmfnfm  19662  flimclslem  19688  fclsopni  19719  fclsnei  19723  fclsbas  19725  fclsrest  19728  fclscmp  19734  ufilcmp  19736  isfcf  19738  fcfnei  19739  fcfneii  19741  ptcmplem2  19756  cnextcn  19770  cnextfres  19771  tsmsfbas  19829  iscusp  20005  cuspcvg  20007  lpbl  20209  prdsxmslem2  20235  restmetu  20293  qdensere  20480  lebnumlem3  20666  isphtpc  20697  iscmet  20926  cmetcvg  20927  equivcmet  20957  cmetcusp1OLD  20994  cmetcusp1  20995  cmetcuspOLD  20996  cmetcusp  20997  rrxmvallem  21034  ovolicc2lem2  21132  ovolicc2lem5  21135  i1fres  21315  lhop1lem  21617  deg1ldg  21695  plyco0  21792  plyeq0lem  21810  coeeq2  21842  coe1termlem  21857  taylfval  21956  cxpeq0  22255  ftalem4  22545  ftalem5  22546  ftalem6  22547  isppw  22584  isnsqf  22605  sqff1o  22652  musum  22663  dchrelbas3  22709  dchrelbasd  22710  dchrelbas4  22714  dchrmulcl  22720  dchrn0  22721  dchrfi  22726  dchrptlem2  22736  dchrpt  22738  lgsne0  22804  lgsdchr  22819  2sqlem11  22846  uvtx01vtx  23551  nmorepnf  24319  nmoprepnf  25422  nmfnrepnf  25435  disjdsct  26148  sibfof  26869  signswch  27105  signstfvneq0  27116  derangenlem  27202  subfacp1lem3  27213  subfacp1lem5  27215  subfacp1lem6  27216  subfacp1  27217  iscvm  27291  cvmcov  27295  cvmcov2  27307  prodfn0  27552  prodfrec  27553  prodfdiv  27554  ntrivcvgtail  27558  fproddiv  27615  fprodn0  27633  eldm3  27715  elima4  27733  nobndlem2  27977  nobndlem4  27979  nobndlem5  27980  nobndlem6  27981  nobndlem8  27983  nobndup  27984  nobnddown  27985  nofulllem5  27990  mblfinlem3  28577  itg2addnclem3  28592  finlocfin  28718  locfincmp  28723  locfindis  28724  neibastop1  28727  neibastop2lem  28728  neibastop2  28729  neibastop3  28730  neifg  28739  sstotbnd2  28820  cntotbnd  28842  heibor1lem  28855  pellexlem3  29319  inisegn0  29543  mncn0  29643  aaitgo  29666  stoweidlem28  29970  stoweidlem43  29985  f12dfv  30293  f13dfv  30294  usg2cwwkdifex  30642  frgraregorufr  30793  clwwlkextfrlem1  30816  numclwwlkovh  30841  numclwwlk2lem1  30842  numclwlk2lem2f  30843  numclwlk2lem2f1o  30845  numclwwlk5  30852  rmsupp0  30928  scmsuppss  30932  suppmptcfin  30940  mptnn0fsuppr  30951  linc1  31077  el0ldep  31118  ldepspr  31125  islindeps2  31135  zlmodzxzldeplem4  31163  zlmodzxzldep  31164  ldepsnlinclem1  31165  ldepsnlinclem2  31166  ldepsnlinc  31168  secval  31395  cscval  31396  cotval  31397  2llnm3N  33536  dalem4  33632  cdlemk28-3  34875  mapdh9a  35758