Theorem neeq1d 2683

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

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1444   =/= wne 2622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-cleq 2444  df-ne 2624

This theorem is referenced by:  neeq1  2686  eqnetrd  2691  prnzg  4092  inisegn0  5200  f12dfv  6172  f13dfv  6173  suppval1  6920  elsuppfn  6922  suppsnop  6928  ressuppss  6934  ressuppssdif  6936  tz7.49  7162  ereldm  7407  pw2f1olem  7676  marypha1lem  7947  wdomtr  8090  inf3lem2  8134  cantnflem1  8194  cantnf  8198  cplem2  8361  dfac9  8566  kmlem12  8591  infpssrlem4  8736  fin23lem14  8763  axcc2lem  8866  axcc3  8868  domtriomlem  8872  axdc2lem  8878  ac6c4  8911  zorn2lem6  8931  rpnnen1lem4  11293  rpnnen1lem5  11294  mptnn0fsuppr  12211  hashprg  12572  hashtpg  12641  prodfn0  13950  prodfrec  13951  prodfdiv  13952  ntrivcvgtail  13956  fproddiv  14015  fprodn0  14033  fproddivf  14041  dvdsle  14350  algcvg  14535  algcvga  14538  eucalgcvga  14545  rpdvds  14676  phibndlem  14718  dfphi2  14722  pcaddlem  14833  vdwmc  14928  iscatd2  15587  brcic  15703  cicer  15711  sgrp2nmndlem5  16663  symgextf1lem  17061  pmtrmvd  17097  frgpup3lem  17427  isirred  17927  isdrngrd  18001  rrgsupp  18515  dsmmelbas  19302  dsmmacl  19304  frlmssuvc2  19353  elcls  20089  clsndisj  20091  elcls3  20099  neindisj2  20139  clslp  20164  cmpfi  20423  cmpfii  20424  dfcon2  20434  consuba  20435  nconsubb  20438  1stcelcls  20476  finlocfin  20535  locfincmp  20541  dissnlocfin  20544  locfindis  20545  ptclsg  20630  dfac14lem  20632  isfbas  20844  trfbas2  20858  isfil  20862  filss  20868  fbunfip  20884  fgval  20885  elfg  20886  isufil2  20923  ufileu  20934  filufint  20935  fmfnfm  20973  flimclslem  20999  fclsopni  21030  fclsnei  21034  fclsbas  21036  fclsrest  21039  fclscmp  21045  ufilcmp  21047  isfcf  21049  fcfnei  21050  fcfneii  21052  ptcmplem2  21068  cnextcn  21082  cnextfres1  21083  tsmsfbas  21142  iscusp  21314  cuspcvg  21316  lpbl  21518  prdsxmslem2  21544  restmetu  21585  qdensere  21790  lebnumlem3  21991  lebnumlem3OLD  21994  isphtpc  22025  iscmet  22254  cmetcvg  22255  equivcmet  22285  cmetcusp1  22320  cmetcusp  22321  rrxmvallem  22358  ovolicc2lem2  22471  ovolicc2lem5  22475  i1fres  22663  lhop1lem  22965  deg1ldg  23041  plyco0  23146  plyeq0lem  23164  coeeq2  23196  coe1termlem  23212  taylfval  23314  cxpeq0  23623  ftalem4  24000  ftalem5  24001  ftalem4OLD  24002  ftalem5OLD  24003  ftalem6  24004  isppw  24041  isnsqf  24062  sqff1o  24109  musum  24120  dchrelbas3  24166  dchrelbasd  24167  dchrelbas4  24171  dchrmulcl  24177  dchrn0  24178  dchrfi  24183  dchrptlem2  24193  dchrpt  24195  lgsne0  24261  lgsdchr  24276  2sqlem11  24303  ishlg  24647  uvtx01vtx  25220  usg2cwwkdifex  25549  frgraregorufr  25781  clwwlkextfrlem1  25804  numclwwlkovh  25829  numclwwlk2lem1  25830  numclwlk2lem2f  25831  numclwlk2lem2f1o  25833  numclwwlk5  25840  nmorepnf  26409  nmoprepnf  27520  nmfnrepnf  27533  disjdsct  28283  locfinreflem  28667  sibfof  29173  signswch  29450  signstfvneq0  29461  derangenlem  29894  subfacp1lem3  29905  subfacp1lem5  29907  subfacp1lem6  29908  subfacp1  29909  iscvm  29982  cvmcov  29986  cvmcov2  29998  eldm3  30402  elima4  30421  nobndlem2  30582  nobndlem4  30584  nobndlem5  30585  nobndlem6  30586  nobndlem8  30588  nobndup  30589  nobnddown  30590  nofulllem5  30595  neibastop1  31015  neibastop2lem  31016  neibastop2  31017  neibastop3  31018  neifg  31027  poimirlem17  31957  poimirlem18  31958  poimirlem20  31960  poimirlem21  31961  poimirlem22  31962  poimirlem23  31963  poimirlem27  31967  poimirlem28  31968  poimirlem30  31970  poimirlem31  31971  poimirlem32  31972  mblfinlem3  31979  itg2addnclem3  31995  sstotbnd2  32106  cntotbnd  32128  heibor1lem  32141  2llnm3N  33134  dalem4  33230  cdlemk28-3  34475  mapdh9a  35358  pellexlem3  35675  mncn0  35998  aaitgo  36028  cvgdvgrat  36662  binomcxplemnotnn0  36705  disjf1  37457  disjrnmpt2  37463  disjinfi  37468  fsumiunss  37654  islptre  37699  islpcn  37719  lptre2pt  37720  0ellimcdiv  37730  stoweidlem28  37888  stoweidlem43  37904  dirkercncflem2  37966  fourierdlem46  38016  fourierdlem79  38049  elaa2lem  38097  elaa2lemOLD  38098  elaa2  38099  sge0fodjrnlem  38258  sge0iunmpt  38260  nnfoctbdjlem  38293  meadjiunlem  38303  meadjiun  38304  uvtxa01vtx0  39469  ovn0ssdmfun  39820  nzerooringczr  40127  rmsupp0  40206  scmsuppss  40210  suppmptcfin  40217  linc1  40271  el0ldep  40312  ldepspr  40319  islindeps2  40329  zlmodzxzldeplem4  40349  zlmodzxzldep  40350  ldepsnlinclem1  40351  ldepsnlinclem2  40352  ldepsnlinc  40354  secval  40520  cscval  40521  cotval  40522