Theorem neeq1d 3041

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1520   ≠ wne 2982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-9 2089  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-cleq 2786  df-ne 2983

This theorem is referenced by:  neeq1  3044  eqnetrd  3049  inisegn0  5829  f12dfv  6886  f13dfv  6887  suppval1  7678  elsuppfn  7680  suppsnop  7686  ressuppss  7691  ressuppssdif  7693  tz7.49  7923  ereldm  8178  pw2f1olem  8458  marypha1lem  8733  wdomtr  8875  inf3lem2  8927  cantnflem1  8987  cantnf  8991  cplem2  9154  dfac9  9397  kmlem12  9422  infpssrlem4  9563  fin23lem14  9590  axcc2lem  9693  axcc3  9695  domtriomlem  9699  axdc2lem  9705  ac6c4  9738  zorn2lem6  9758  rpnnen1lem4  12218  rpnnen1lem5  12219  mptnn0fsuppr  13205  hashprg  13592  hashtpg  13677  prodfn0  15071  prodfrec  15072  prodfdiv  15073  ntrivcvgtail  15077  fproddiv  15136  fprodn0  15154  fproddivf  15162  dvdsle  15481  algcvg  15737  algcvga  15740  eucalgcvga  15747  rpdvds  15821  phibndlem  15924  dfphi2  15928  pcaddlem  16041  vdwmc  16131  iscatd2  16769  brcic  16885  cicer  16893  sgrp2nmndlem5  17843  symgextf1lem  18267  pmtrmvd  18303  frgpup3lem  18618  isirred  19127  isdrngrd  19206  rrgsupp  19741  dsmmelbas  20553  dsmmacl  20555  frlmssuvc2  20609  elcls  21353  clsndisj  21355  elcls3  21363  neindisj2  21403  clslp  21428  cmpfi  21688  cmpfii  21689  dfconn2  21699  connsuba  21700  nconnsubb  21703  1stcelcls  21741  finlocfin  21800  locfincmp  21806  dissnlocfin  21809  locfindis  21810  ptclsg  21895  dfac14lem  21897  isfbas  22109  trfbas2  22123  isfil  22127  filss  22133  fbunfip  22149  fgval  22150  elfg  22151  isufil2  22188  ufileu  22199  filufint  22200  fmfnfm  22238  flimclslem  22264  fclsopni  22295  fclsnei  22299  fclsbas  22301  fclsrest  22304  fclscmp  22310  ufilcmp  22312  isfcf  22314  fcfnei  22315  fcfneii  22317  ptcmplem2  22333  cnextcn  22347  cnextfres1  22348  tsmsfbas  22407  iscusp  22579  cuspcvg  22581  lpbl  22784  prdsxmslem2  22810  restmetu  22851  qdensere  23049  lebnumlem3  23238  isphtpc  23269  iscmet  23558  cmetcvg  23559  equivcmet  23591  cmetcusp1  23627  cmetcusp  23628  rrxmvallem  23678  ovolicc2lem2  23790  ovolicc2lem5  23793  i1fres  23977  lhop1lem  24281  deg1ldg  24357  plyco0  24453  plyeq0lem  24471  coeeq2  24503  coe1termlem  24519  taylfval  24618  cxpeq0  24930  ftalem4  25323  ftalem5  25324  ftalem6  25325  isppw  25361  isnsqf  25382  sqff1o  25429  musum  25438  dchrelbas3  25484  dchrelbasd  25485  dchrelbas4  25489  dchrmulcl  25495  dchrn0  25496  dchrfi  25501  dchrptlem2  25511  dchrpt  25513  lgsne0  25581  lgsdchr  25601  2sqlem11  25675  ishlg  26058  uvtx01vtx  26850  pthdlem2lem  27223  2pthdlem1  27384  clwwlknclwwlkdif  27432  umgr2cwwkdifex  27519  3pthdlem1  27618  frgrregorufr  27784  numclwwlk2lem1lem  27801  numclwwlk2lem1  27835  numclwlk2lem2f  27836  numclwlk2lem2f1o  27838  nmorepnf  28224  nmoprepnf  29323  nmfnrepnf  29336  disjdsct  30099  rmfsupp2  30475  fedgmullem2  30585  locfinreflem  30677  sibfof  31171  signswch  31404  signstfvneq0  31415  derangenlem  31982  subfacp1lem3  31993  subfacp1lem5  31995  subfacp1lem6  31996  subfacp1  31997  iscvm  32070  cvmcov  32074  cvmcov2  32086  eldm3  32550  elima4  32572  nosupbnd2lem1  32769  neibastop1  33261  neibastop2lem  33262  neibastop2  33263  neibastop3  33264  neifg  33273  poimirlem17  34386  poimirlem18  34387  poimirlem20  34389  poimirlem21  34390  poimirlem22  34391  poimirlem23  34392  poimirlem27  34396  poimirlem28  34397  poimirlem30  34399  poimirlem31  34400  poimirlem32  34401  mblfinlem3  34408  itg2addnclem3  34422  sstotbnd2  34530  cntotbnd  34552  heibor1lem  34565  dmecd  35042  br1cosscnvxrn  35195  2llnm3N  36186  dalem4  36282  cdlemk28-3  37525  mapdh9a  38406  dffltz  38718  pellexlem3  38864  mncn0  39175  aaitgo  39198  gneispace0nelrn2  39927  cvgdvgrat  40135  binomcxplemnotnn0  40178  disjf1  40936  disjrnmpt2  40942  disjinfi  40947  fsumiunss  41352  islptre  41396  islpcn  41416  lptre2pt  41417  0ellimcdiv  41426  liminflelimsup  41553  stoweidlem28  41809  stoweidlem43  41824  dirkercncflem2  41885  fourierdlem46  41933  fourierdlem79  41966  elaa2lem  42014  elaa2  42015  sge0fodjrnlem  42194  sge0iunmpt  42196  nnfoctbdjlem  42233  meadjiunlem  42243  meadjiun  42244  ovn0ssdmfun  43470  nzerooringczr  43775  rmsupp0  43850  scmsuppss  43854  suppmptcfin  43861  linc1  43914  el0ldep  43955  ldepspr  43962  islindeps2  43972  zlmodzxzldeplem4  43992  zlmodzxzldep  43993  ldepsnlinclem1  43994  ldepsnlinclem2  43995  ldepsnlinc  43997  secval  44280  cscval  44281  cotval  44282