Theorem neeq1d 2616

Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.)

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	. 2 |- ( ph -> A = B )
2		neeq1 2611	. 2 |- ( A = B -> ( A =/= C <-> B =/= C ) )
3	1, 2	syl 16	1 |- ( ph -> ( A =/= C <-> B =/= C ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1369   =/= wne 2601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2431  df-ne 2603

This theorem is referenced by:  neeq12d  2618  eqnetrd  2621  prnzg  3990  suppval1  6691  elsuppfn  6693  suppsnop  6699  ressuppss  6703  ressuppssdif  6705  tz7.49  6892  ereldm  7136  pw2f1olem  7407  marypha1lem  7675  wdomtr  7782  inf3lem2  7827  cantnflem1  7889  cantnf  7893  cantnfOLD  7915  cplem2  8089  dfac9  8297  kmlem12  8322  infpssrlem4  8467  fin23lem14  8494  axcc2lem  8597  axcc3  8599  domtriomlem  8603  axdc2lem  8609  ac6c4  8642  zorn2lem6  8662  rpnnen1lem4  10974  rpnnen1lem5  10975  hashprg  12147  hashtpg  12178  dvdsle  13570  algcvg  13743  algcvga  13746  eucalgcvga  13753  rpdvds  13802  phibndlem  13837  dfphi2  13841  pcaddlem  13942  vdwmc  14031  iscatd2  14611  symgextf1lem  15916  pmtrmvd  15953  frgpup3lem  16265  isirred  16779  isdrngrd  16836  rrgsupp  17339  dsmmelbas  18139  dsmmacl  18141  frlmssuvc2  18195  frlmssuvc2OLD  18197  elcls  18652  clsndisj  18654  elcls3  18662  neindisj2  18702  clslp  18727  cmpfi  18986  cmpfii  18987  dfcon2  18998  consuba  18999  nconsubb  19002  1stcelcls  19040  ptclsg  19163  dfac14lem  19165  isfbas  19377  trfbas2  19391  isfil  19395  filss  19401  fbunfip  19417  fgval  19418  elfg  19419  isufil2  19456  ufileu  19467  filufint  19468  fmfnfm  19506  flimclslem  19532  fclsopni  19563  fclsnei  19567  fclsbas  19569  fclsrest  19572  fclscmp  19578  ufilcmp  19580  isfcf  19582  fcfnei  19583  fcfneii  19585  ptcmplem2  19600  cnextcn  19614  cnextfres  19615  tsmsfbas  19673  iscusp  19849  cuspcvg  19851  lpbl  20053  prdsxmslem2  20079  restmetu  20137  qdensere  20324  lebnumlem3  20510  isphtpc  20541  iscmet  20770  cmetcvg  20771  equivcmet  20801  cmetcusp1OLD  20838  cmetcusp1  20839  cmetcuspOLD  20840  cmetcusp  20841  rrxmvallem  20878  ovolicc2lem2  20976  ovolicc2lem5  20979  i1fres  21158  lhop1lem  21460  deg1ldg  21538  plyco0  21635  plyeq0lem  21653  coeeq2  21685  coe1termlem  21700  taylfval  21799  cxpeq0  22098  ftalem4  22388  ftalem5  22389  ftalem6  22390  isppw  22427  isnsqf  22448  sqff1o  22495  musum  22506  dchrelbas3  22552  dchrelbasd  22553  dchrelbas4  22557  dchrmulcl  22563  dchrn0  22564  dchrfi  22569  dchrptlem2  22579  dchrpt  22581  lgsne0  22647  lgsdchr  22662  2sqlem11  22689  uvtx01vtx  23351  nmorepnf  24119  nmoprepnf  25222  nmfnrepnf  25235  disjdsct  25949  sibfof  26678  signswch  26914  signstfvneq0  26925  derangenlem  27011  subfacp1lem3  27022  subfacp1lem5  27024  subfacp1lem6  27025  subfacp1  27026  iscvm  27100  cvmcov  27104  cvmcov2  27116  prodfn0  27360  prodfrec  27361  prodfdiv  27362  ntrivcvgtail  27366  fproddiv  27423  fprodn0  27441  eldm3  27523  elima4  27541  nobndlem2  27785  nobndlem4  27787  nobndlem5  27788  nobndlem6  27789  nobndlem8  27791  nobndup  27792  nobnddown  27793  nofulllem5  27798  mblfinlem3  28383  itg2addnclem3  28398  finlocfin  28524  locfincmp  28529  locfindis  28530  neibastop1  28533  neibastop2lem  28534  neibastop2  28535  neibastop3  28536  neifg  28545  sstotbnd2  28626  cntotbnd  28648  heibor1lem  28661  pellexlem3  29125  inisegn0  29349  mncn0  29449  aaitgo  29472  stoweidlem28  29776  stoweidlem43  29791  f12dfv  30099  f13dfv  30100  usg2cwwkdifex  30448  frgraregorufr  30599  clwwlkextfrlem1  30622  numclwwlkovh  30647  numclwwlk2lem1  30648  numclwlk2lem2f  30649  numclwlk2lem2f1o  30651  numclwwlk5  30658  rmsupp0  30732  scmsuppss  30736  suppmptcfin  30743  linc1  30848  el0ldep  30889  ldepspr  30896  islindeps2  30906  zlmodzxzldeplem4  30934  zlmodzxzldep  30935  ldepsnlinclem1  30936  ldepsnlinclem2  30937  ldepsnlinc  30939  secval  30971  cscval  30972  cotval  30973  2llnm3N  33053  dalem4  33149  cdlemk28-3  34392  mapdh9a  35275