Theorem neeq1d 2744

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   =/= wne 2662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664

This theorem is referenced by:  neeq12dOLD  2747  neeq1  2748  eqnetrd  2760  prnzg  4147  f12dfv  6167  f13dfv  6168  suppval1  6907  elsuppfn  6909  suppsnop  6915  ressuppss  6919  ressuppssdif  6921  tz7.49  7110  ereldm  7355  pw2f1olem  7621  marypha1lem  7893  wdomtr  8001  inf3lem2  8046  cantnflem1  8108  cantnf  8112  cantnfOLD  8134  cplem2  8308  dfac9  8516  kmlem12  8541  infpssrlem4  8686  fin23lem14  8713  axcc2lem  8816  axcc3  8818  domtriomlem  8822  axdc2lem  8828  ac6c4  8861  zorn2lem6  8881  rpnnen1lem4  11211  rpnnen1lem5  11212  mptnn0fsuppr  12073  hashprg  12428  hashtpg  12489  dvdsle  13890  algcvg  14064  algcvga  14067  eucalgcvga  14074  rpdvds  14124  phibndlem  14159  dfphi2  14163  pcaddlem  14266  vdwmc  14355  iscatd2  14936  symgextf1lem  16250  pmtrmvd  16287  frgpup3lem  16601  isirred  17149  isdrngrd  17222  rrgsupp  17738  dsmmelbas  18565  dsmmacl  18567  frlmssuvc2  18621  frlmssuvc2OLD  18623  elcls  19368  clsndisj  19370  elcls3  19378  neindisj2  19418  clslp  19443  cmpfi  19702  cmpfii  19703  dfcon2  19714  consuba  19715  nconsubb  19718  1stcelcls  19756  ptclsg  19879  dfac14lem  19881  isfbas  20093  trfbas2  20107  isfil  20111  filss  20117  fbunfip  20133  fgval  20134  elfg  20135  isufil2  20172  ufileu  20183  filufint  20184  fmfnfm  20222  flimclslem  20248  fclsopni  20279  fclsnei  20283  fclsbas  20285  fclsrest  20288  fclscmp  20294  ufilcmp  20296  isfcf  20298  fcfnei  20299  fcfneii  20301  ptcmplem2  20316  cnextcn  20330  cnextfres  20331  tsmsfbas  20389  iscusp  20565  cuspcvg  20567  lpbl  20769  prdsxmslem2  20795  restmetu  20853  qdensere  21040  lebnumlem3  21226  isphtpc  21257  iscmet  21486  cmetcvg  21487  equivcmet  21517  cmetcusp1OLD  21554  cmetcusp1  21555  cmetcuspOLD  21556  cmetcusp  21557  rrxmvallem  21594  ovolicc2lem2  21692  ovolicc2lem5  21695  i1fres  21875  lhop1lem  22177  deg1ldg  22255  plyco0  22352  plyeq0lem  22370  coeeq2  22402  coe1termlem  22417  taylfval  22516  cxpeq0  22815  ftalem4  23105  ftalem5  23106  ftalem6  23107  isppw  23144  isnsqf  23165  sqff1o  23212  musum  23223  dchrelbas3  23269  dchrelbasd  23270  dchrelbas4  23274  dchrmulcl  23280  dchrn0  23281  dchrfi  23286  dchrptlem2  23296  dchrpt  23298  lgsne0  23364  lgsdchr  23379  2sqlem11  23406  uvtx01vtx  24196  usg2cwwkdifex  24525  frgraregorufr  24758  clwwlkextfrlem1  24781  numclwwlkovh  24806  numclwwlk2lem1  24807  numclwlk2lem2f  24808  numclwlk2lem2f1o  24810  numclwwlk5  24817  nmorepnf  25387  nmoprepnf  26490  nmfnrepnf  26503  disjdsct  27221  sibfof  27950  signswch  28186  signstfvneq0  28197  derangenlem  28283  subfacp1lem3  28294  subfacp1lem5  28296  subfacp1lem6  28297  subfacp1  28298  iscvm  28372  cvmcov  28376  cvmcov2  28388  prodfn0  28633  prodfrec  28634  prodfdiv  28635  ntrivcvgtail  28639  fproddiv  28696  fprodn0  28714  eldm3  28796  elima4  28814  nobndlem2  29058  nobndlem4  29060  nobndlem5  29061  nobndlem6  29062  nobndlem8  29064  nobndup  29065  nobnddown  29066  nofulllem5  29071  mblfinlem3  29658  itg2addnclem3  29673  finlocfin  29799  locfincmp  29804  locfindis  29805  neibastop1  29808  neibastop2lem  29809  neibastop2  29810  neibastop3  29811  neifg  29820  sstotbnd2  29901  cntotbnd  29923  heibor1lem  29936  pellexlem3  30399  inisegn0  30621  mncn0  30721  aaitgo  30744  islptre  31189  islpcn  31209  lptre2pt  31210  0ellimcdiv  31219  stoweidlem28  31356  stoweidlem43  31371  dirkercncflem2  31432  fourierdlem43  31478  fourierdlem46  31481  fourierdlem79  31514  rmsupp0  32060  scmsuppss  32064  suppmptcfin  32071  linc1  32125  el0ldep  32166  ldepspr  32173  islindeps2  32183  zlmodzxzldeplem4  32203  zlmodzxzldep  32204  ldepsnlinclem1  32205  ldepsnlinclem2  32206  ldepsnlinc  32208  secval  32240  cscval  32241  cotval  32242  2llnm3N  34383  dalem4  34479  cdlemk28-3  35722  mapdh9a  36605