Theorem neeq1d 2731

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1398   =/= wne 2649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-ne 2651

This theorem is referenced by:  neeq12dOLD  2734  neeq1  2735  eqnetrd  2747  prnzg  4136  f12dfv  6154  f13dfv  6155  suppval1  6897  elsuppfn  6899  suppsnop  6905  ressuppss  6911  ressuppssdif  6913  tz7.49  7102  ereldm  7347  pw2f1olem  7614  marypha1lem  7885  wdomtr  7993  inf3lem2  8037  cantnflem1  8099  cantnf  8103  cantnfOLD  8125  cplem2  8299  dfac9  8507  kmlem12  8532  infpssrlem4  8677  fin23lem14  8704  axcc2lem  8807  axcc3  8809  domtriomlem  8813  axdc2lem  8819  ac6c4  8852  zorn2lem6  8872  rpnnen1lem4  11212  rpnnen1lem5  11213  mptnn0fsuppr  12087  hashprg  12444  hashtpg  12507  prodfn0  13785  prodfrec  13786  prodfdiv  13787  ntrivcvgtail  13791  fproddiv  13848  fprodn0  13865  dvdsle  14115  algcvg  14289  algcvga  14292  eucalgcvga  14299  rpdvds  14349  phibndlem  14384  dfphi2  14388  pcaddlem  14491  vdwmc  14580  iscatd2  15170  brcic  15286  cicer  15294  sgrp2nmndlem5  16246  symgextf1lem  16644  pmtrmvd  16680  frgpup3lem  16994  isirred  17543  isdrngrd  17617  rrgsupp  18134  dsmmelbas  18943  dsmmacl  18945  frlmssuvc2  18997  elcls  19741  clsndisj  19743  elcls3  19751  neindisj2  19791  clslp  19816  cmpfi  20075  cmpfii  20076  dfcon2  20086  consuba  20087  nconsubb  20090  1stcelcls  20128  finlocfin  20187  locfincmp  20193  dissnlocfin  20196  locfindis  20197  ptclsg  20282  dfac14lem  20284  isfbas  20496  trfbas2  20510  isfil  20514  filss  20520  fbunfip  20536  fgval  20537  elfg  20538  isufil2  20575  ufileu  20586  filufint  20587  fmfnfm  20625  flimclslem  20651  fclsopni  20682  fclsnei  20686  fclsbas  20688  fclsrest  20691  fclscmp  20697  ufilcmp  20699  isfcf  20701  fcfnei  20702  fcfneii  20704  ptcmplem2  20719  cnextcn  20733  cnextfres  20734  tsmsfbas  20792  iscusp  20968  cuspcvg  20970  lpbl  21172  prdsxmslem2  21198  restmetu  21256  qdensere  21443  lebnumlem3  21629  isphtpc  21660  iscmet  21889  cmetcvg  21890  equivcmet  21920  cmetcusp1OLD  21957  cmetcusp1  21958  cmetcuspOLD  21959  cmetcusp  21960  rrxmvallem  21997  ovolicc2lem2  22095  ovolicc2lem5  22098  i1fres  22278  lhop1lem  22580  deg1ldg  22658  plyco0  22755  plyeq0lem  22773  coeeq2  22805  coe1termlem  22821  taylfval  22920  cxpeq0  23227  ftalem4  23547  ftalem5  23548  ftalem6  23549  isppw  23586  isnsqf  23607  sqff1o  23654  musum  23665  dchrelbas3  23711  dchrelbasd  23712  dchrelbas4  23716  dchrmulcl  23722  dchrn0  23723  dchrfi  23728  dchrptlem2  23738  dchrpt  23740  lgsne0  23806  lgsdchr  23821  2sqlem11  23848  ishlg  24187  uvtx01vtx  24694  usg2cwwkdifex  25023  frgraregorufr  25255  clwwlkextfrlem1  25278  numclwwlkovh  25303  numclwwlk2lem1  25304  numclwlk2lem2f  25305  numclwlk2lem2f1o  25307  numclwwlk5  25314  nmorepnf  25881  nmoprepnf  26984  nmfnrepnf  26997  disjdsct  27749  locfinreflem  28078  sibfof  28546  signswch  28782  signstfvneq0  28793  derangenlem  28879  subfacp1lem3  28890  subfacp1lem5  28892  subfacp1lem6  28893  subfacp1  28894  iscvm  28968  cvmcov  28972  cvmcov2  28984  eldm3  29432  elima4  29449  nobndlem2  29693  nobndlem4  29695  nobndlem5  29696  nobndlem6  29697  nobndlem8  29699  nobndup  29700  nobnddown  29701  nofulllem5  29706  mblfinlem3  30293  itg2addnclem3  30308  neibastop1  30417  neibastop2lem  30418  neibastop2  30419  neibastop3  30420  neifg  30429  sstotbnd2  30510  cntotbnd  30532  heibor1lem  30545  pellexlem3  31006  inisegn0  31228  mncn0  31329  aaitgo  31352  cvgdvgrat  31435  binomcxplemnotnn0  31502  fproddivf  31827  islptre  31864  islpcn  31884  lptre2pt  31885  0ellimcdiv  31894  stoweidlem28  32049  stoweidlem43  32064  dirkercncflem2  32125  fourierdlem46  32174  fourierdlem79  32207  elaa2lem  32255  elaa2  32256  ovn0ssdmfun  32827  nzerooringczr  33134  rmsupp0  33215  scmsuppss  33219  suppmptcfin  33226  linc1  33280  el0ldep  33321  ldepspr  33328  islindeps2  33338  zlmodzxzldeplem4  33358  zlmodzxzldep  33359  ldepsnlinclem1  33360  ldepsnlinclem2  33361  ldepsnlinc  33363  secval  33531  cscval  33532  cotval  33533  2llnm3N  35690  dalem4  35786  cdlemk28-3  37031  mapdh9a  37914