Theorem neeq1d 3033

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

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637   ≠ wne 2974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-ext 2781

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2795  df-ne 2975

This theorem is referenced by:  neeq1  3036  eqnetrd  3041  inisegn0  5701  f12dfv  6747  f13dfv  6748  suppval1  7529  elsuppfn  7531  suppsnop  7537  ressuppss  7542  ressuppssdif  7544  tz7.49  7770  ereldm  8019  pw2f1olem  8297  marypha1lem  8572  wdomtr  8713  inf3lem2  8767  cantnflem1  8827  cantnf  8831  cplem2  8994  dfac9  9237  kmlem12  9262  infpssrlem4  9407  fin23lem14  9434  axcc2lem  9537  axcc3  9539  domtriomlem  9543  axdc2lem  9549  ac6c4  9582  zorn2lem6  9602  rpnnen1lem4  12030  rpnnen1lem5  12031  mptnn0fsuppr  13016  hashprg  13394  hashtpg  13478  prodfn0  14841  prodfrec  14842  prodfdiv  14843  ntrivcvgtail  14847  fproddiv  14906  fprodn0  14924  fproddivf  14932  dvdsle  15249  algcvg  15502  algcvga  15505  eucalgcvga  15512  rpdvds  15586  phibndlem  15686  dfphi2  15690  pcaddlem  15803  vdwmc  15893  iscatd2  16540  brcic  16656  cicer  16664  sgrp2nmndlem5  17615  symgextf1lem  18035  pmtrmvd  18071  frgpup3lem  18385  isirred  18895  isdrngrd  18971  rrgsupp  19494  dsmmelbas  20287  dsmmacl  20289  frlmssuvc2  20338  elcls  21085  clsndisj  21087  elcls3  21095  neindisj2  21135  clslp  21160  cmpfi  21419  cmpfii  21420  dfconn2  21430  connsuba  21431  nconnsubb  21434  1stcelcls  21472  finlocfin  21531  locfincmp  21537  dissnlocfin  21540  locfindis  21541  ptclsg  21626  dfac14lem  21628  isfbas  21840  trfbas2  21854  isfil  21858  filss  21864  fbunfip  21880  fgval  21881  elfg  21882  isufil2  21919  ufileu  21930  filufint  21931  fmfnfm  21969  flimclslem  21995  fclsopni  22026  fclsnei  22030  fclsbas  22032  fclsrest  22035  fclscmp  22041  ufilcmp  22043  isfcf  22045  fcfnei  22046  fcfneii  22048  ptcmplem2  22064  cnextcn  22078  cnextfres1  22079  tsmsfbas  22138  iscusp  22310  cuspcvg  22312  lpbl  22515  prdsxmslem2  22541  restmetu  22582  qdensere  22780  lebnumlem3  22969  isphtpc  23000  iscmet  23288  cmetcvg  23289  equivcmet  23320  cmetcusp1  23355  cmetcusp  23356  rrxmvallem  23393  ovolicc2lem2  23493  ovolicc2lem5  23496  i1fres  23680  lhop1lem  23984  deg1ldg  24060  plyco0  24156  plyeq0lem  24174  coeeq2  24206  coe1termlem  24222  taylfval  24321  cxpeq0  24632  ftalem4  25010  ftalem5  25011  ftalem6  25012  isppw  25048  isnsqf  25069  sqff1o  25116  musum  25125  dchrelbas3  25171  dchrelbasd  25172  dchrelbas4  25176  dchrmulcl  25182  dchrn0  25183  dchrfi  25188  dchrptlem2  25198  dchrpt  25200  lgsne0  25268  lgsdchr  25288  2sqlem11  25362  ishlg  25705  uvtx01vtx  26512  uvtxa01vtx0OLD  26514  pthdlem2lem  26885  2pthdlem1  27064  clwwlknclwwlkdif  27114  umgr2cwwkdifex  27210  clwlksfclwwlkOLD  27230  3pthdlem1  27331  frgrregorufr  27494  numclwwlk2lem1lem  27512  numclwwlk2lem1lemOLD  27513  numclwwlk2lem1  27550  numclwlk2lem2f  27551  numclwlk2lem2f1o  27553  numclwwlkovhOLD  27556  numclwwlk2lem1OLD  27557  numclwlk2lem2fOLD  27558  numclwlk2lem2f1oOLD  27560  nmorepnf  27945  nmoprepnf  29048  nmfnrepnf  29061  disjdsct  29801  locfinreflem  30226  sibfof  30721  signswch  30957  signstfvneq0  30968  derangenlem  31470  subfacp1lem3  31481  subfacp1lem5  31483  subfacp1lem6  31484  subfacp1  31485  iscvm  31558  cvmcov  31562  cvmcov2  31574  eldm3  31967  elima4  31993  nosupbnd2lem1  32176  neibastop1  32669  neibastop2lem  32670  neibastop2  32671  neibastop3  32672  neifg  32681  poimirlem17  33733  poimirlem18  33734  poimirlem20  33736  poimirlem21  33737  poimirlem22  33738  poimirlem23  33739  poimirlem27  33743  poimirlem28  33744  poimirlem30  33746  poimirlem31  33747  poimirlem32  33748  mblfinlem3  33755  itg2addnclem3  33769  sstotbnd2  33878  cntotbnd  33900  heibor1lem  33913  dmecd  34384  br1cosscnvxrn  34531  2llnm3N  35343  dalem4  35439  cdlemk28-3  36683  mapdh9a  37564  pellexlem3  37891  mncn0  38204  aaitgo  38227  gneispace0nelrn2  38933  cvgdvgrat  39006  binomcxplemnotnn0  39049  disjf1  39852  disjrnmpt2  39858  disjinfi  39863  fsumiunss  40281  islptre  40325  islpcn  40345  lptre2pt  40346  0ellimcdiv  40355  liminflelimsup  40482  stoweidlem28  40718  stoweidlem43  40733  dirkercncflem2  40794  fourierdlem46  40842  fourierdlem79  40875  elaa2lem  40923  elaa2  40924  sge0fodjrnlem  41106  sge0iunmpt  41108  nnfoctbdjlem  41145  meadjiunlem  41155  meadjiun  41156  ovn0ssdmfun  42329  nzerooringczr  42634  rmsupp0  42711  scmsuppss  42715  suppmptcfin  42722  linc1  42776  el0ldep  42817  ldepspr  42824  islindeps2  42834  zlmodzxzldeplem4  42854  zlmodzxzldep  42855  ldepsnlinclem1  42856  ldepsnlinclem2  42857  ldepsnlinc  42859  secval  43053  cscval  43054  cotval  43055