Theorem neeq1d 3019

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ≠ wne 2960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ne 2961

This theorem is referenced by:  neeq1  3022  eqnetrd  3027  iftrueb  4496  inisegn0  6091  f1ounsn  7260  f12dfv  7261  f13dfv  7262  resf1extb  7919  suppval1  8150  elsuppfng  8153  elsuppfn  8154  suppsnop  8162  ressuppss  8167  ressuppssdif  8169  tz7.49  8420  ereldm  8736  pw2f1olem  9057  marypha1lem  9381  wdomtr  9525  inf3lem2  9586  cantnflem1  9646  cantnf  9650  cplem2  9864  dfac9  10108  kmlem12  10133  infpssrlem4  10278  fin23lem14  10305  axcc2lem  10408  axcc3  10410  domtriomlem  10414  axdc2lem  10420  ac6c4  10453  zorn2lem6  10473  rpnnen1lem4  12995  rpnnen1lem5  12996  mptnn0fsuppr  14026  hashprg  14422  hashtpg  14512  prodfn0  15938  prodfrec  15939  prodfdiv  15940  ntrivcvgtail  15944  fproddiv  16005  fprodn0  16023  fproddivf  16031  dvdsle  16358  algcvg  16624  algcvga  16627  eucalgcvga  16634  rpdvds  16708  phibndlem  16819  dfphi2  16823  pcaddlem  16938  vdwmc  17028  iscatd2  17727  brcic  17845  cicer  17853  cat1lem  18143  cat1  18144  sgrp2nmndlem5  18981  symgextf1lem  19481  pmtrmvd  19517  frgpup3lem  19838  isirred  20492  rrgsupp  20777  isdrngrd  20839  isdrngrdOLD  20841  nzerooringczr  21590  dsmmelbas  21849  dsmmacl  21851  frlmssuvc2  21905  mhpsclcl  22270  mhpmulcl  22272  elcls  23191  clsndisj  23193  elcls3  23201  neindisj2  23241  clslp  23266  cmpfi  23526  cmpfii  23527  dfconn2  23537  connsuba  23538  nconnsubb  23541  1stcelcls  23579  finlocfin  23638  locfincmp  23644  dissnlocfin  23647  locfindis  23648  ptclsg  23733  dfac14lem  23735  isfbas  23947  trfbas2  23961  isfil  23965  filss  23971  fbunfip  23987  fgval  23988  elfg  23989  isufil2  24026  ufileu  24037  filufint  24038  fmfnfm  24076  flimclslem  24102  fclsopni  24133  fclsnei  24137  fclsbas  24139  fclsrest  24142  fclscmp  24148  ufilcmp  24150  isfcf  24152  fcfnei  24153  fcfneii  24155  ptcmplem2  24171  cnextcn  24185  cnextfres1  24186  tsmsfbas  24246  iscusp  24416  cuspcvg  24418  lpbl  24621  prdsxmslem2  24647  restmetu  24688  qdensere  24887  lebnumlem3  25083  isphtpc  25114  iscmet  25404  cmetcvg  25405  equivcmet  25437  cmetcusp1  25473  cmetcusp  25474  rrxmvallem  25524  ovolicc2lem2  25638  ovolicc2lem5  25641  i1fres  25825  lhop1lem  26133  deg1ldg  26210  plyco0  26310  plyeq0lem  26328  coeeq2  26360  coe1termlem  26376  taylfval  26480  cxpeq0  26801  ftalem4  27198  ftalem5  27199  ftalem6  27200  isppw  27236  isnsqf  27257  sqff1o  27304  musum  27313  dchrelbas3  27360  dchrelbasd  27361  dchrelbas4  27365  dchrmulcl  27371  dchrn0  27372  dchrfi  27377  dchrptlem2  27387  dchrpt  27389  lgsne0  27457  lgsdchr  27477  2sqlem11  27551  nosupbnd2lem1  27837  expsne0  28587  ishlg  28829  uvtx01vtx  29656  pthdlem2lem  30025  2pthdlem1  30188  clwwlknclwwlkdif  30239  umgr2cwwkdifex  30325  3pthdlem1  30424  frgrregorufr  30585  numclwwlk2lem1lem  30602  numclwwlk2lem1  30636  numclwlk2lem2f  30637  numclwlk2lem2f1o  30639  nmorepnf  31029  nmoprepnf  32128  nmfnrepnf  32141  fdifsupp  32942  ressupprn  32947  disjdsct  32960  suppgsumssiun  33305  rmfsupp2  33470  domnprodn0  33511  isufd  33747  ufdprmidl  33748  1arithufdlem4  33754  dfufd2lem  33756  fedgmullem2  33937  constrconj  34052  constrelextdg2  34054  constrllcllem  34059  constrcbvlem  34062  locfinreflem  34147  sibfof  34647  signswch  34865  signstfvneq0  34876  vonf1wev  35463  vonf1owevOLD  35465  derangenlem  35534  subfacp1lem3  35545  subfacp1lem5  35547  subfacp1lem6  35548  subfacp1  35549  iscvm  35622  cvmcov  35626  cvmcov2  35638  eldm3  36124  elima4  36139  neibastop1  36732  neibastop2lem  36733  neibastop2  36734  neibastop3  36735  neifg  36744  dfttc4lem1  36901  dfttc4lem2  36902  poimirlem17  38148  poimirlem18  38149  poimirlem20  38151  poimirlem21  38152  poimirlem22  38153  poimirlem23  38154  poimirlem27  38158  poimirlem28  38159  poimirlem30  38161  poimirlem31  38162  poimirlem32  38163  mblfinlem3  38170  itg2addnclem3  38184  sstotbnd2  38285  cntotbnd  38307  heibor1lem  38320  dmecd  38821  disjecxrn  38923  br1cosscnvxrn  39075  disjimeceqim  39315  eldisjim3  39326  2llnm3N  40205  dalem4  40301  cdlemk28-3  41544  mapdh9a  42425  idomnnzpownz  42761  idomnnzgmulnz  42762  sticksstones1  42775  aks6d1c6lem1  42799  unitscyglem2  42825  unitscyglem3  42826  unitscyglem4  42827  readvcot  42985  domnexpgn0cl  43153  fsuppind  43184  dffltz  43228  pellexlem3  43420  mncn0  43728  aaitgo  43751  gneispace0nelrn2  44729  cvgdvgrat  44887  binomcxplemnotnn0  44930  disjf1  45759  disjrnmpt2  45764  disjinfi  45768  fsumiunss  46149  islptre  46193  islpcn  46211  lptre2pt  46212  0ellimcdiv  46221  liminflelimsup  46348  stoweidlem28  46600  stoweidlem43  46615  dirkercncflem2  46676  fourierdlem46  46724  fourierdlem79  46757  elaa2lem  46805  elaa2  46806  sge0fodjrnlem  46988  sge0iunmpt  46990  nnfoctbdjlem  47027  meadjiunlem  47037  meadjiun  47038  gpg5nbgrvtx13starlem1  48691  gpg5nbgrvtx13starlem3  48693  ovn0ssdmfun  48779  rmsupp0  48999  scmsuppss  49002  suppmptcfin  49007  linc1  49056  el0ldep  49097  ldepspr  49104  islindeps2  49114  zlmodzxzldeplem4  49134  zlmodzxzldep  49135  ldepsnlinclem1  49136  ldepsnlinclem2  49137  ldepsnlinc  49139  fvconstr  49491  fvconstrn0  49492  fvconstr2  49493  catprslem  49639  catprsc  49642  catprsc2  49643  oppccic  49673  relcic  49674  cicpropdlem  49678  secval  50376  cscval  50377  cotval  50378