Theorem neeq1d 3004

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 2741	. 2 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	2	necon3bid 2989	1 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ≠ wne 2944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-ne 2945

This theorem is referenced by:  neeq1  3007  eqnetrd  3012  inisegn0  6009  f12dfv  7154  f13dfv  7155  suppval1  7992  elsuppfng  7995  elsuppfn  7996  suppsnop  8003  ressuppss  8008  ressuppssdif  8010  tz7.49  8285  ereldm  8555  pw2f1olem  8872  marypha1lem  9201  wdomtr  9343  inf3lem2  9396  cantnflem1  9456  cantnf  9460  cplem2  9657  dfac9  9901  kmlem12  9926  infpssrlem4  10071  fin23lem14  10098  axcc2lem  10201  axcc3  10203  domtriomlem  10207  axdc2lem  10213  ac6c4  10246  zorn2lem6  10266  rpnnen1lem4  12729  rpnnen1lem5  12730  mptnn0fsuppr  13728  hashprg  14119  hashtpg  14208  prodfn0  15615  prodfrec  15616  prodfdiv  15617  ntrivcvgtail  15621  fproddiv  15680  fprodn0  15698  fproddivf  15706  dvdsle  16028  algcvg  16290  algcvga  16293  eucalgcvga  16300  rpdvds  16374  phibndlem  16480  dfphi2  16484  pcaddlem  16598  vdwmc  16688  iscatd2  17399  brcic  17519  cicer  17527  cat1lem  17820  cat1  17821  sgrp2nmndlem5  18577  symgextf1lem  19037  pmtrmvd  19073  frgpup3lem  19392  isirred  19950  isdrngrd  20026  rrgsupp  20571  dsmmelbas  20955  dsmmacl  20957  frlmssuvc2  21011  mhpsclcl  21346  mhpmulcl  21348  elcls  22233  clsndisj  22235  elcls3  22243  neindisj2  22283  clslp  22308  cmpfi  22568  cmpfii  22569  dfconn2  22579  connsuba  22580  nconnsubb  22583  1stcelcls  22621  finlocfin  22680  locfincmp  22686  dissnlocfin  22689  locfindis  22690  ptclsg  22775  dfac14lem  22777  isfbas  22989  trfbas2  23003  isfil  23007  filss  23013  fbunfip  23029  fgval  23030  elfg  23031  isufil2  23068  ufileu  23079  filufint  23080  fmfnfm  23118  flimclslem  23144  fclsopni  23175  fclsnei  23179  fclsbas  23181  fclsrest  23184  fclscmp  23190  ufilcmp  23192  isfcf  23194  fcfnei  23195  fcfneii  23197  ptcmplem2  23213  cnextcn  23227  cnextfres1  23228  tsmsfbas  23288  iscusp  23460  cuspcvg  23462  lpbl  23668  prdsxmslem2  23694  restmetu  23735  qdensere  23942  lebnumlem3  24135  isphtpc  24166  iscmet  24457  cmetcvg  24458  equivcmet  24490  cmetcusp1  24526  cmetcusp  24527  rrxmvallem  24577  ovolicc2lem2  24691  ovolicc2lem5  24694  i1fres  24879  lhop1lem  25186  deg1ldg  25266  plyco0  25362  plyeq0lem  25380  coeeq2  25412  coe1termlem  25428  taylfval  25527  cxpeq0  25842  ftalem4  26234  ftalem5  26235  ftalem6  26236  isppw  26272  isnsqf  26293  sqff1o  26340  musum  26349  dchrelbas3  26395  dchrelbasd  26396  dchrelbas4  26400  dchrmulcl  26406  dchrn0  26407  dchrfi  26412  dchrptlem2  26422  dchrpt  26424  lgsne0  26492  lgsdchr  26512  2sqlem11  26586  ishlg  26972  uvtx01vtx  27773  pthdlem2lem  28144  2pthdlem1  28304  clwwlknclwwlkdif  28352  umgr2cwwkdifex  28438  3pthdlem1  28537  frgrregorufr  28698  numclwwlk2lem1lem  28715  numclwwlk2lem1  28749  numclwlk2lem2f  28750  numclwlk2lem2f1o  28752  nmorepnf  29139  nmoprepnf  30238  nmfnrepnf  30251  ressupprn  31033  disjdsct  31044  rmfsupp2  31501  isufd  31672  fedgmullem2  31720  locfinreflem  31799  sibfof  32316  signswch  32549  signstfvneq0  32560  derangenlem  33142  subfacp1lem3  33153  subfacp1lem5  33155  subfacp1lem6  33156  subfacp1  33157  iscvm  33230  cvmcov  33234  cvmcov2  33246  eldm3  33737  elima4  33759  nosupbnd2lem1  33927  neibastop1  34557  neibastop2lem  34558  neibastop2  34559  neibastop3  34560  neifg  34569  poimirlem17  35803  poimirlem18  35804  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem23  35809  poimirlem27  35813  poimirlem28  35814  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  mblfinlem3  35825  itg2addnclem3  35839  sstotbnd2  35941  cntotbnd  35963  heibor1lem  35976  dmecd  36447  br1cosscnvxrn  36599  2llnm3N  37590  dalem4  37686  cdlemk28-3  38929  mapdh9a  39810  sticksstones1  40109  metakunt29  40160  fsuppind  40286  dffltz  40478  pellexlem3  40660  mncn0  40971  aaitgo  40994  gneispace0nelrn2  41758  cvgdvgrat  41938  binomcxplemnotnn0  41981  disjf1  42727  disjrnmpt2  42733  disjinfi  42738  fsumiunss  43123  islptre  43167  islpcn  43187  lptre2pt  43188  0ellimcdiv  43197  liminflelimsup  43324  stoweidlem28  43576  stoweidlem43  43591  dirkercncflem2  43652  fourierdlem46  43700  fourierdlem79  43733  elaa2lem  43781  elaa2  43782  sge0fodjrnlem  43961  sge0iunmpt  43963  nnfoctbdjlem  44000  meadjiunlem  44010  meadjiun  44011  ovn0ssdmfun  45332  nzerooringczr  45641  rmsupp0  45715  scmsuppss  45719  suppmptcfin  45726  linc1  45777  el0ldep  45818  ldepspr  45825  islindeps2  45835  zlmodzxzldeplem4  45855  zlmodzxzldep  45856  ldepsnlinclem1  45857  ldepsnlinclem2  45858  ldepsnlinc  45860  fvconstr  46194  fvconstrn0  46195  fvconstr2  46196  catprslem  46302  catprsc  46305  catprsc2  46306  secval  46460  cscval  46461  cotval  46462