Theorem neeq1d 2992

Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Hypothesis

Ref	Expression
neeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
neeq1d	⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Proof of Theorem neeq1d

Step	Hyp	Ref	Expression
1		neeq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqeq1d 2739	. 2 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	2	necon3bid 2977	1 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  neeq1  2995  eqnetrd  3000  iftrueb  4494  inisegn0  6065  f1ounsn  7228  f12dfv  7229  f13dfv  7230  resf1extb  7886  suppval1  8118  elsuppfng  8121  elsuppfn  8122  suppsnop  8130  ressuppss  8135  ressuppssdif  8137  tz7.49  8386  ereldm  8699  pw2f1olem  9021  marypha1lem  9348  wdomtr  9492  inf3lem2  9550  cantnflem1  9610  cantnf  9614  cplem2  9814  dfac9  10059  kmlem12  10084  infpssrlem4  10228  fin23lem14  10255  axcc2lem  10358  axcc3  10360  domtriomlem  10364  axdc2lem  10370  ac6c4  10403  zorn2lem6  10423  rpnnen1lem4  12905  rpnnen1lem5  12906  mptnn0fsuppr  13934  hashprg  14330  hashtpg  14420  prodfn0  15829  prodfrec  15830  prodfdiv  15831  ntrivcvgtail  15835  fproddiv  15896  fprodn0  15914  fproddivf  15922  dvdsle  16249  algcvg  16515  algcvga  16518  eucalgcvga  16525  rpdvds  16599  phibndlem  16709  dfphi2  16713  pcaddlem  16828  vdwmc  16918  iscatd2  17616  brcic  17734  cicer  17742  cat1lem  18032  cat1  18033  sgrp2nmndlem5  18866  symgextf1lem  19361  pmtrmvd  19397  frgpup3lem  19718  isirred  20367  rrgsupp  20646  isdrngrd  20711  isdrngrdOLD  20713  nzerooringczr  21447  dsmmelbas  21706  dsmmacl  21708  frlmssuvc2  21762  mhpsclcl  22102  mhpmulcl  22104  elcls  23029  clsndisj  23031  elcls3  23039  neindisj2  23079  clslp  23104  cmpfi  23364  cmpfii  23365  dfconn2  23375  connsuba  23376  nconnsubb  23379  1stcelcls  23417  finlocfin  23476  locfincmp  23482  dissnlocfin  23485  locfindis  23486  ptclsg  23571  dfac14lem  23573  isfbas  23785  trfbas2  23799  isfil  23803  filss  23809  fbunfip  23825  fgval  23826  elfg  23827  isufil2  23864  ufileu  23875  filufint  23876  fmfnfm  23914  flimclslem  23940  fclsopni  23971  fclsnei  23975  fclsbas  23977  fclsrest  23980  fclscmp  23986  ufilcmp  23988  isfcf  23990  fcfnei  23991  fcfneii  23993  ptcmplem2  24009  cnextcn  24023  cnextfres1  24024  tsmsfbas  24084  iscusp  24254  cuspcvg  24256  lpbl  24459  prdsxmslem2  24485  restmetu  24526  qdensere  24725  lebnumlem3  24930  isphtpc  24961  iscmet  25252  cmetcvg  25253  equivcmet  25285  cmetcusp1  25321  cmetcusp  25322  rrxmvallem  25372  ovolicc2lem2  25487  ovolicc2lem5  25490  i1fres  25674  lhop1lem  25986  deg1ldg  26065  plyco0  26165  plyeq0lem  26183  coeeq2  26215  coe1termlem  26231  taylfval  26334  cxpeq0  26655  ftalem4  27054  ftalem5  27055  ftalem6  27056  isppw  27092  isnsqf  27113  sqff1o  27160  musum  27169  dchrelbas3  27217  dchrelbasd  27218  dchrelbas4  27222  dchrmulcl  27228  dchrn0  27229  dchrfi  27234  dchrptlem2  27244  dchrpt  27246  lgsne0  27314  lgsdchr  27334  2sqlem11  27408  nosupbnd2lem1  27695  expsne0  28444  ishlg  28686  uvtx01vtx  29482  pthdlem2lem  29852  2pthdlem1  30015  clwwlknclwwlkdif  30066  umgr2cwwkdifex  30152  3pthdlem1  30251  frgrregorufr  30412  numclwwlk2lem1lem  30429  numclwwlk2lem1  30463  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  nmorepnf  30855  nmoprepnf  31954  nmfnrepnf  31967  fdifsupp  32774  ressupprn  32779  disjdsct  32792  suppgsumssiun  33165  rmfsupp2  33331  domnprodn0  33368  isufd  33632  ufdprmidl  33633  1arithufdlem4  33639  dfufd2lem  33641  fedgmullem2  33807  constrconj  33922  constrelextdg2  33924  constrllcllem  33929  constrcbvlem  33932  locfinreflem  34017  sibfof  34517  signswch  34738  signstfvneq0  34749  vonf1owev  35321  derangenlem  35384  subfacp1lem3  35395  subfacp1lem5  35397  subfacp1lem6  35398  subfacp1  35399  iscvm  35472  cvmcov  35476  cvmcov2  35488  eldm3  35974  elima4  35989  neibastop1  36572  neibastop2lem  36573  neibastop2  36574  neibastop3  36575  neifg  36584  poimirlem17  37882  poimirlem18  37883  poimirlem20  37885  poimirlem21  37886  poimirlem22  37887  poimirlem23  37888  poimirlem27  37892  poimirlem28  37893  poimirlem30  37895  poimirlem31  37896  poimirlem32  37897  mblfinlem3  37904  itg2addnclem3  37918  sstotbnd2  38019  cntotbnd  38041  heibor1lem  38054  dmecd  38555  disjecxrn  38657  br1cosscnvxrn  38809  disjimeceqim  39049  eldisjim3  39060  2llnm3N  39939  dalem4  40035  cdlemk28-3  41278  mapdh9a  42159  idomnnzpownz  42496  idomnnzgmulnz  42497  sticksstones1  42510  aks6d1c6lem1  42534  unitscyglem2  42560  unitscyglem3  42561  unitscyglem4  42562  readvcot  42728  domnexpgn0cl  42887  fsuppind  42942  dffltz  42986  pellexlem3  43182  mncn0  43490  aaitgo  43513  gneispace0nelrn2  44491  cvgdvgrat  44663  binomcxplemnotnn0  44706  disjf1  45536  disjrnmpt2  45541  disjinfi  45545  fsumiunss  45929  islptre  45973  islpcn  45991  lptre2pt  45992  0ellimcdiv  46001  liminflelimsup  46128  stoweidlem28  46380  stoweidlem43  46395  dirkercncflem2  46456  fourierdlem46  46504  fourierdlem79  46537  elaa2lem  46585  elaa2  46586  sge0fodjrnlem  46768  sge0iunmpt  46770  nnfoctbdjlem  46807  meadjiunlem  46817  meadjiun  46818  gpg5nbgrvtx13starlem1  48425  gpg5nbgrvtx13starlem3  48427  ovn0ssdmfun  48513  rmsupp0  48722  scmsuppss  48725  suppmptcfin  48730  linc1  48779  el0ldep  48820  ldepspr  48827  islindeps2  48837  zlmodzxzldeplem4  48857  zlmodzxzldep  48858  ldepsnlinclem1  48859  ldepsnlinclem2  48860  ldepsnlinc  48862  fvconstr  49215  fvconstrn0  49216  fvconstr2  49217  catprslem  49363  catprsc  49366  catprsc2  49367  oppccic  49397  relcic  49398  cicpropdlem  49402  secval  50100  cscval  50101  cotval  50102