Theorem neeq1d 2997

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ne 2938

This theorem is referenced by:  neeq1  3000  eqnetrd  3005  inisegn0  6118  f1ounsn  7291  f12dfv  7292  f13dfv  7293  suppval1  8189  elsuppfng  8192  elsuppfn  8193  suppsnop  8201  ressuppss  8206  ressuppssdif  8208  tz7.49  8483  ereldm  8793  pw2f1olem  9114  marypha1lem  9470  wdomtr  9612  inf3lem2  9666  cantnflem1  9726  cantnf  9730  cplem2  9927  dfac9  10174  kmlem12  10199  infpssrlem4  10343  fin23lem14  10370  axcc2lem  10473  axcc3  10475  domtriomlem  10479  axdc2lem  10485  ac6c4  10518  zorn2lem6  10538  rpnnen1lem4  13019  rpnnen1lem5  13020  mptnn0fsuppr  14036  hashprg  14430  hashtpg  14520  prodfn0  15926  prodfrec  15927  prodfdiv  15928  ntrivcvgtail  15932  fproddiv  15993  fprodn0  16011  fproddivf  16019  dvdsle  16343  algcvg  16609  algcvga  16612  eucalgcvga  16619  rpdvds  16693  phibndlem  16803  dfphi2  16807  pcaddlem  16921  vdwmc  17011  iscatd2  17725  brcic  17845  cicer  17853  cat1lem  18149  cat1  18150  sgrp2nmndlem5  18954  symgextf1lem  19452  pmtrmvd  19488  frgpup3lem  19809  isirred  20435  rrgsupp  20717  isdrngrd  20782  isdrngrdOLD  20784  nzerooringczr  21508  dsmmelbas  21776  dsmmacl  21778  frlmssuvc2  21832  mhpsclcl  22168  mhpmulcl  22170  elcls  23096  clsndisj  23098  elcls3  23106  neindisj2  23146  clslp  23171  cmpfi  23431  cmpfii  23432  dfconn2  23442  connsuba  23443  nconnsubb  23446  1stcelcls  23484  finlocfin  23543  locfincmp  23549  dissnlocfin  23552  locfindis  23553  ptclsg  23638  dfac14lem  23640  isfbas  23852  trfbas2  23866  isfil  23870  filss  23876  fbunfip  23892  fgval  23893  elfg  23894  isufil2  23931  ufileu  23942  filufint  23943  fmfnfm  23981  flimclslem  24007  fclsopni  24038  fclsnei  24042  fclsbas  24044  fclsrest  24047  fclscmp  24053  ufilcmp  24055  isfcf  24057  fcfnei  24058  fcfneii  24060  ptcmplem2  24076  cnextcn  24090  cnextfres1  24091  tsmsfbas  24151  iscusp  24323  cuspcvg  24325  lpbl  24531  prdsxmslem2  24557  restmetu  24598  qdensere  24805  lebnumlem3  25008  isphtpc  25039  iscmet  25331  cmetcvg  25332  equivcmet  25364  cmetcusp1  25400  cmetcusp  25401  rrxmvallem  25451  ovolicc2lem2  25566  ovolicc2lem5  25569  i1fres  25754  lhop1lem  26066  deg1ldg  26145  plyco0  26245  plyeq0lem  26263  coeeq2  26295  coe1termlem  26311  taylfval  26414  cxpeq0  26734  ftalem4  27133  ftalem5  27134  ftalem6  27135  isppw  27171  isnsqf  27192  sqff1o  27239  musum  27248  dchrelbas3  27296  dchrelbasd  27297  dchrelbas4  27301  dchrmulcl  27307  dchrn0  27308  dchrfi  27313  dchrptlem2  27323  dchrpt  27325  lgsne0  27393  lgsdchr  27413  2sqlem11  27487  nosupbnd2lem1  27774  expsne0  28428  ishlg  28624  uvtx01vtx  29428  pthdlem2lem  29799  2pthdlem1  29959  clwwlknclwwlkdif  30007  umgr2cwwkdifex  30093  3pthdlem1  30192  frgrregorufr  30353  numclwwlk2lem1lem  30370  numclwwlk2lem1  30404  numclwlk2lem2f  30405  numclwlk2lem2f1o  30407  nmorepnf  30796  nmoprepnf  31895  nmfnrepnf  31908  fdifsupp  32699  ressupprn  32704  disjdsct  32717  rmfsupp2  33227  domnprodn0  33261  isufd  33547  ufdprmidl  33548  1arithufdlem4  33554  dfufd2lem  33556  fedgmullem2  33657  constrconj  33749  constrelextdg2  33751  locfinreflem  33800  sibfof  34321  signswch  34554  signstfvneq0  34565  derangenlem  35155  subfacp1lem3  35166  subfacp1lem5  35168  subfacp1lem6  35169  subfacp1  35170  iscvm  35243  cvmcov  35247  cvmcov2  35259  eldm3  35740  elima4  35756  neibastop1  36341  neibastop2lem  36342  neibastop2  36343  neibastop3  36344  neifg  36353  poimirlem17  37623  poimirlem18  37624  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem27  37633  poimirlem28  37634  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  mblfinlem3  37645  itg2addnclem3  37659  sstotbnd2  37760  cntotbnd  37782  heibor1lem  37795  dmecd  38285  disjecxrn  38370  br1cosscnvxrn  38455  2llnm3N  39551  dalem4  39647  cdlemk28-3  40890  mapdh9a  41771  idomnnzpownz  42113  idomnnzgmulnz  42114  sticksstones1  42127  aks6d1c6lem1  42151  unitscyglem2  42177  unitscyglem3  42178  unitscyglem4  42179  metakunt29  42214  domnexpgn0cl  42509  fsuppind  42576  dffltz  42620  pellexlem3  42818  mncn0  43127  aaitgo  43150  gneispace0nelrn2  44130  cvgdvgrat  44308  binomcxplemnotnn0  44351  disjf1  45125  disjrnmpt2  45130  disjinfi  45134  fsumiunss  45530  islptre  45574  islpcn  45594  lptre2pt  45595  0ellimcdiv  45604  liminflelimsup  45731  stoweidlem28  45983  stoweidlem43  45998  dirkercncflem2  46059  fourierdlem46  46107  fourierdlem79  46140  elaa2lem  46188  elaa2  46189  sge0fodjrnlem  46371  sge0iunmpt  46373  nnfoctbdjlem  46410  meadjiunlem  46420  meadjiun  46421  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem3  47963  ovn0ssdmfun  48002  rmsupp0  48212  scmsuppss  48215  suppmptcfin  48220  linc1  48270  el0ldep  48311  ldepspr  48318  islindeps2  48328  zlmodzxzldeplem4  48348  zlmodzxzldep  48349  ldepsnlinclem1  48350  ldepsnlinclem2  48351  ldepsnlinc  48353  fvconstr  48685  fvconstrn0  48686  fvconstr2  48687  catprslem  48798  catprsc  48801  catprsc2  48802  secval  48977  cscval  48978  cotval  48979