Theorem neeq1d 2853

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

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  neeq1  2856  eqnetrd  2861  prnzgOLD  4312  inisegn0  5497  f12dfv  6529  f13dfv  6530  suppval1  7301  elsuppfn  7303  suppsnop  7309  ressuppss  7314  ressuppssdif  7316  tz7.49  7540  ereldm  7790  pw2f1olem  8064  marypha1lem  8339  wdomtr  8480  inf3lem2  8526  cantnflem1  8586  cantnf  8590  cplem2  8753  dfac9  8958  kmlem12  8983  infpssrlem4  9128  fin23lem14  9155  axcc2lem  9258  axcc3  9260  domtriomlem  9264  axdc2lem  9270  ac6c4  9303  zorn2lem6  9323  rpnnen1lem4  11817  rpnnen1lem5  11818  rpnnen1lem4OLD  11823  rpnnen1lem5OLD  11824  mptnn0fsuppr  12799  hashprg  13182  hashprgOLD  13183  hashtpg  13267  prodfn0  14626  prodfrec  14627  prodfdiv  14628  ntrivcvgtail  14632  fproddiv  14691  fprodn0  14709  fproddivf  14718  dvdsle  15032  algcvg  15289  algcvga  15292  eucalgcvga  15299  rpdvds  15374  phibndlem  15475  dfphi2  15479  pcaddlem  15592  vdwmc  15682  iscatd2  16342  brcic  16458  cicer  16466  sgrp2nmndlem5  17416  symgextf1lem  17840  pmtrmvd  17876  frgpup3lem  18190  isirred  18699  isdrngrd  18773  rrgsupp  19291  dsmmelbas  20083  dsmmacl  20085  frlmssuvc2  20134  elcls  20877  clsndisj  20879  elcls3  20887  neindisj2  20927  clslp  20952  cmpfi  21211  cmpfii  21212  dfconn2  21222  connsuba  21223  nconnsubb  21226  1stcelcls  21264  finlocfin  21323  locfincmp  21329  dissnlocfin  21332  locfindis  21333  ptclsg  21418  dfac14lem  21420  isfbas  21633  trfbas2  21647  isfil  21651  filss  21657  fbunfip  21673  fgval  21674  elfg  21675  isufil2  21712  ufileu  21723  filufint  21724  fmfnfm  21762  flimclslem  21788  fclsopni  21819  fclsnei  21823  fclsbas  21825  fclsrest  21828  fclscmp  21834  ufilcmp  21836  isfcf  21838  fcfnei  21839  fcfneii  21841  ptcmplem2  21857  cnextcn  21871  cnextfres1  21872  tsmsfbas  21931  iscusp  22103  cuspcvg  22105  lpbl  22308  prdsxmslem2  22334  restmetu  22375  qdensere  22573  lebnumlem3  22762  isphtpc  22793  iscmet  23082  cmetcvg  23083  equivcmet  23114  cmetcusp1  23149  cmetcusp  23150  rrxmvallem  23187  ovolicc2lem2  23286  ovolicc2lem5  23289  i1fres  23472  lhop1lem  23776  deg1ldg  23852  plyco0  23948  plyeq0lem  23966  coeeq2  23998  coe1termlem  24014  taylfval  24113  cxpeq0  24424  ftalem4  24802  ftalem5  24803  ftalem6  24804  isppw  24840  isnsqf  24861  sqff1o  24908  musum  24917  dchrelbas3  24963  dchrelbasd  24964  dchrelbas4  24968  dchrmulcl  24974  dchrn0  24975  dchrfi  24980  dchrptlem2  24990  dchrpt  24992  lgsne0  25060  lgsdchr  25080  2sqlem11  25154  ishlg  25497  uvtxa01vtx0  26297  pthdlem2lem  26663  2pthdlem1  26826  umgr2cwwkdifex  26942  clwlksfclwwlk  26962  3pthdlem1  27024  frgrregorufr  27189  clwwlkextfrlem1  27208  numclwwlkovh  27234  numclwwlk2lem1  27235  numclwlk2lem2f  27236  numclwlk2lem2f1o  27238  nmorepnf  27623  nmoprepnf  28726  nmfnrepnf  28739  disjdsct  29480  locfinreflem  29907  sibfof  30402  signswch  30638  signstfvneq0  30649  derangenlem  31153  subfacp1lem3  31164  subfacp1lem5  31166  subfacp1lem6  31167  subfacp1  31168  iscvm  31241  cvmcov  31245  cvmcov2  31257  eldm3  31651  elima4  31679  nosupbnd2lem1  31861  neibastop1  32354  neibastop2lem  32355  neibastop2  32356  neibastop3  32357  neifg  32366  poimirlem17  33426  poimirlem18  33427  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem23  33432  poimirlem27  33436  poimirlem28  33437  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  mblfinlem3  33448  itg2addnclem3  33463  sstotbnd2  33573  cntotbnd  33595  heibor1lem  33608  dmecd  34074  2llnm3N  34855  dalem4  34951  cdlemk28-3  36196  mapdh9a  37079  pellexlem3  37395  mncn0  37709  aaitgo  37732  gneispace0nelrn2  38439  cvgdvgrat  38512  binomcxplemnotnn0  38555  disjf1  39369  disjrnmpt2  39375  disjinfi  39380  fsumiunss  39807  islptre  39851  islpcn  39871  lptre2pt  39872  0ellimcdiv  39881  liminflelimsup  40008  stoweidlem28  40245  stoweidlem43  40260  dirkercncflem2  40321  fourierdlem46  40369  fourierdlem79  40402  elaa2lem  40450  elaa2  40451  sge0fodjrnlem  40633  sge0iunmpt  40635  nnfoctbdjlem  40672  meadjiunlem  40682  meadjiun  40683  ovn0ssdmfun  41767  nzerooringczr  42072  rmsupp0  42149  scmsuppss  42153  suppmptcfin  42160  linc1  42214  el0ldep  42255  ldepspr  42262  islindeps2  42272  zlmodzxzldeplem4  42292  zlmodzxzldep  42293  ldepsnlinclem1  42294  ldepsnlinclem2  42295  ldepsnlinc  42297  secval  42488  cscval  42489  cotval  42490