Theorem neeq1d 2611

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 2606	. 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 1362   =/= wne 2596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-ex 1590  df-cleq 2426  df-ne 2598

This theorem is referenced by:  neeq12d  2613  eqnetrd  2616  prnzg  3983  suppval1  6685  elsuppfn  6687  suppsnop  6693  ressuppss  6697  ressuppssdif  6699  tz7.49  6886  ereldm  7132  pw2f1olem  7403  marypha1lem  7671  wdomtr  7778  inf3lem2  7823  cantnflem1  7885  cantnf  7889  cantnfOLD  7911  cplem2  8085  dfac9  8293  kmlem12  8318  infpssrlem4  8463  fin23lem14  8490  axcc2lem  8593  axcc3  8595  domtriomlem  8599  axdc2lem  8605  ac6c4  8638  zorn2lem6  8658  rpnnen1lem4  10970  rpnnen1lem5  10971  hashprg  12139  hashtpg  12170  dvdsle  13561  algcvg  13734  algcvga  13737  eucalgcvga  13744  rpdvds  13793  phibndlem  13828  dfphi2  13832  pcaddlem  13933  vdwmc  14022  iscatd2  14602  symgextf1lem  15905  pmtrmvd  15942  frgpup3lem  16254  isirred  16725  isdrngrd  16782  rrgsupp  17284  dsmmelbas  18006  dsmmacl  18008  frlmssuvc2  18062  frlmssuvc2OLD  18064  elcls  18519  clsndisj  18521  elcls3  18529  neindisj2  18569  clslp  18594  cmpfi  18853  cmpfii  18854  dfcon2  18865  consuba  18866  nconsubb  18869  1stcelcls  18907  ptclsg  19030  dfac14lem  19032  isfbas  19244  trfbas2  19258  isfil  19262  filss  19268  fbunfip  19284  fgval  19285  elfg  19286  isufil2  19323  ufileu  19334  filufint  19335  fmfnfm  19373  flimclslem  19399  fclsopni  19430  fclsnei  19434  fclsbas  19436  fclsrest  19439  fclscmp  19445  ufilcmp  19447  isfcf  19449  fcfnei  19450  fcfneii  19452  ptcmplem2  19467  cnextcn  19481  cnextfres  19482  tsmsfbas  19540  iscusp  19716  cuspcvg  19718  lpbl  19920  prdsxmslem2  19946  restmetu  20004  qdensere  20191  lebnumlem3  20377  isphtpc  20408  iscmet  20637  cmetcvg  20638  equivcmet  20668  cmetcusp1OLD  20705  cmetcusp1  20706  cmetcuspOLD  20707  cmetcusp  20708  rrxmvallem  20745  ovolicc2lem2  20843  ovolicc2lem5  20846  i1fres  21025  lhop1lem  21327  deg1ldg  21448  plyco0  21545  plyeq0lem  21563  coeeq2  21595  coe1termlem  21610  taylfval  21709  cxpeq0  22008  ftalem4  22298  ftalem5  22299  ftalem6  22300  isppw  22337  isnsqf  22358  sqff1o  22405  musum  22416  dchrelbas3  22462  dchrelbasd  22463  dchrelbas4  22467  dchrmulcl  22473  dchrn0  22474  dchrfi  22479  dchrptlem2  22489  dchrpt  22491  lgsne0  22557  lgsdchr  22572  2sqlem11  22599  uvtx01vtx  23223  nmorepnf  23991  nmoprepnf  25094  nmfnrepnf  25107  disjdsct  25822  sibfof  26574  signswch  26810  signstfvneq0  26821  derangenlem  26907  subfacp1lem3  26918  subfacp1lem5  26920  subfacp1lem6  26921  subfacp1  26922  iscvm  26996  cvmcov  27000  cvmcov2  27012  prodfn0  27256  prodfrec  27257  prodfdiv  27258  ntrivcvgtail  27262  fproddiv  27319  fprodn0  27337  eldm3  27419  elima4  27437  nobndlem2  27681  nobndlem4  27683  nobndlem5  27684  nobndlem6  27685  nobndlem8  27687  nobndup  27688  nobnddown  27689  nofulllem5  27694  mblfinlem3  28274  itg2addnclem3  28289  finlocfin  28415  locfincmp  28420  locfindis  28421  neibastop1  28424  neibastop2lem  28425  neibastop2  28426  neibastop3  28427  neifg  28436  sstotbnd2  28517  cntotbnd  28539  heibor1lem  28552  pellexlem3  29017  inisegn0  29241  mncn0  29341  aaitgo  29364  stoweidlem28  29669  stoweidlem43  29684  f12dfv  29992  f13dfv  29993  usg2cwwkdifex  30341  frgraregorufr  30492  clwwlkextfrlem1  30515  numclwwlkovh  30540  numclwwlk2lem1  30541  numclwlk2lem2f  30542  numclwlk2lem2f1o  30544  numclwwlk5  30551  rmsupp0  30613  scmsuppss  30617  suppmptcfin  30624  linc1  30689  el0ldep  30730  ldepspr  30737  islindeps2  30747  zlmodzxzldeplem4  30775  zlmodzxzldep  30776  ldepsnlinclem1  30777  ldepsnlinclem2  30778  ldepsnlinc  30780  secval  30812  cscval  30813  cotval  30814  2llnm3N  32807  dalem4  32903  cdlemk28-3  34146  mapdh9a  35029