Theorem neeq1d 3001

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 2986	1 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ≠ wne 2941

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1782  df-cleq 2729  df-ne 2942

This theorem is referenced by:  neeq1  3004  eqnetrd  3009  inisegn0  6043  f12dfv  7210  f13dfv  7211  suppval1  8062  elsuppfng  8065  elsuppfn  8066  suppsnop  8073  ressuppss  8078  ressuppssdif  8080  tz7.49  8355  ereldm  8626  pw2f1olem  8950  marypha1lem  9299  wdomtr  9441  inf3lem2  9495  cantnflem1  9555  cantnf  9559  cplem2  9756  dfac9  10002  kmlem12  10027  infpssrlem4  10172  fin23lem14  10199  axcc2lem  10302  axcc3  10304  domtriomlem  10308  axdc2lem  10314  ac6c4  10347  zorn2lem6  10367  rpnnen1lem4  12830  rpnnen1lem5  12831  mptnn0fsuppr  13829  hashprg  14219  hashtpg  14308  prodfn0  15710  prodfrec  15711  prodfdiv  15712  ntrivcvgtail  15716  fproddiv  15775  fprodn0  15793  fproddivf  15801  dvdsle  16123  algcvg  16383  algcvga  16386  eucalgcvga  16393  rpdvds  16467  phibndlem  16573  dfphi2  16577  pcaddlem  16691  vdwmc  16781  iscatd2  17492  brcic  17612  cicer  17620  cat1lem  17913  cat1  17914  sgrp2nmndlem5  18669  symgextf1lem  19129  pmtrmvd  19165  frgpup3lem  19483  isirred  20040  isdrngrd  20126  rrgsupp  20672  dsmmelbas  21056  dsmmacl  21058  frlmssuvc2  21112  mhpsclcl  21447  mhpmulcl  21449  elcls  22334  clsndisj  22336  elcls3  22344  neindisj2  22384  clslp  22409  cmpfi  22669  cmpfii  22670  dfconn2  22680  connsuba  22681  nconnsubb  22684  1stcelcls  22722  finlocfin  22781  locfincmp  22787  dissnlocfin  22790  locfindis  22791  ptclsg  22876  dfac14lem  22878  isfbas  23090  trfbas2  23104  isfil  23108  filss  23114  fbunfip  23130  fgval  23131  elfg  23132  isufil2  23169  ufileu  23180  filufint  23181  fmfnfm  23219  flimclslem  23245  fclsopni  23276  fclsnei  23280  fclsbas  23282  fclsrest  23285  fclscmp  23291  ufilcmp  23293  isfcf  23295  fcfnei  23296  fcfneii  23298  ptcmplem2  23314  cnextcn  23328  cnextfres1  23329  tsmsfbas  23389  iscusp  23561  cuspcvg  23563  lpbl  23769  prdsxmslem2  23795  restmetu  23836  qdensere  24043  lebnumlem3  24236  isphtpc  24267  iscmet  24558  cmetcvg  24559  equivcmet  24591  cmetcusp1  24627  cmetcusp  24628  rrxmvallem  24678  ovolicc2lem2  24792  ovolicc2lem5  24795  i1fres  24980  lhop1lem  25287  deg1ldg  25367  plyco0  25463  plyeq0lem  25481  coeeq2  25513  coe1termlem  25529  taylfval  25628  cxpeq0  25943  ftalem4  26335  ftalem5  26336  ftalem6  26337  isppw  26373  isnsqf  26394  sqff1o  26441  musum  26450  dchrelbas3  26496  dchrelbasd  26497  dchrelbas4  26501  dchrmulcl  26507  dchrn0  26508  dchrfi  26513  dchrptlem2  26523  dchrpt  26525  lgsne0  26593  lgsdchr  26613  2sqlem11  26687  nosupbnd2lem1  26973  ishlg  27318  uvtx01vtx  28119  pthdlem2lem  28489  2pthdlem1  28649  clwwlknclwwlkdif  28697  umgr2cwwkdifex  28783  3pthdlem1  28882  frgrregorufr  29043  numclwwlk2lem1lem  29060  numclwwlk2lem1  29094  numclwlk2lem2f  29095  numclwlk2lem2f1o  29097  nmorepnf  29484  nmoprepnf  30583  nmfnrepnf  30596  ressupprn  31375  disjdsct  31386  rmfsupp2  31843  isufd  32024  fedgmullem2  32073  locfinreflem  32152  sibfof  32671  signswch  32904  signstfvneq0  32915  derangenlem  33496  subfacp1lem3  33507  subfacp1lem5  33509  subfacp1lem6  33510  subfacp1  33511  iscvm  33584  cvmcov  33588  cvmcov2  33600  eldm3  34082  elima4  34098  neibastop1  34687  neibastop2lem  34688  neibastop2  34689  neibastop3  34690  neifg  34699  poimirlem17  35950  poimirlem18  35951  poimirlem20  35953  poimirlem21  35954  poimirlem22  35955  poimirlem23  35956  poimirlem27  35960  poimirlem28  35961  poimirlem30  35963  poimirlem31  35964  poimirlem32  35965  mblfinlem3  35972  itg2addnclem3  35986  sstotbnd2  36088  cntotbnd  36110  heibor1lem  36123  dmecd  36621  disjecxrn  36707  br1cosscnvxrn  36792  2llnm3N  37888  dalem4  37984  cdlemk28-3  39227  mapdh9a  40108  sticksstones1  40410  metakunt29  40461  fsuppind  40590  dffltz  40784  pellexlem3  40966  mncn0  41278  aaitgo  41301  gneispace0nelrn2  42124  cvgdvgrat  42304  binomcxplemnotnn0  42347  disjf1  43099  disjrnmpt2  43105  disjinfi  43110  fsumiunss  43504  islptre  43548  islpcn  43568  lptre2pt  43569  0ellimcdiv  43578  liminflelimsup  43705  stoweidlem28  43957  stoweidlem43  43972  dirkercncflem2  44033  fourierdlem46  44081  fourierdlem79  44114  elaa2lem  44162  elaa2  44163  sge0fodjrnlem  44343  sge0iunmpt  44345  nnfoctbdjlem  44382  meadjiunlem  44392  meadjiun  44393  ovn0ssdmfun  45739  nzerooringczr  46048  rmsupp0  46122  scmsuppss  46126  suppmptcfin  46133  linc1  46184  el0ldep  46225  ldepspr  46232  islindeps2  46242  zlmodzxzldeplem4  46262  zlmodzxzldep  46263  ldepsnlinclem1  46264  ldepsnlinclem2  46265  ldepsnlinc  46267  fvconstr  46600  fvconstrn0  46601  fvconstr2  46602  catprslem  46708  catprsc  46711  catprsc2  46712  secval  46866  cscval  46867  cotval  46868