Theorem neeq1d 2988

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ≠ wne 2929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ne 2930

This theorem is referenced by:  neeq1  2991  eqnetrd  2996  iftrueb  4487  inisegn0  6051  f1ounsn  7212  f12dfv  7213  f13dfv  7214  resf1extb  7870  suppval1  8102  elsuppfng  8105  elsuppfn  8106  suppsnop  8114  ressuppss  8119  ressuppssdif  8121  tz7.49  8370  ereldm  8681  pw2f1olem  9001  marypha1lem  9324  wdomtr  9468  inf3lem2  9526  cantnflem1  9586  cantnf  9590  cplem2  9790  dfac9  10035  kmlem12  10060  infpssrlem4  10204  fin23lem14  10231  axcc2lem  10334  axcc3  10336  domtriomlem  10340  axdc2lem  10346  ac6c4  10379  zorn2lem6  10399  rpnnen1lem4  12880  rpnnen1lem5  12881  mptnn0fsuppr  13908  hashprg  14304  hashtpg  14394  prodfn0  15803  prodfrec  15804  prodfdiv  15805  ntrivcvgtail  15809  fproddiv  15870  fprodn0  15888  fproddivf  15896  dvdsle  16223  algcvg  16489  algcvga  16492  eucalgcvga  16499  rpdvds  16573  phibndlem  16683  dfphi2  16687  pcaddlem  16802  vdwmc  16892  iscatd2  17589  brcic  17707  cicer  17715  cat1lem  18005  cat1  18006  sgrp2nmndlem5  18839  symgextf1lem  19334  pmtrmvd  19370  frgpup3lem  19691  isirred  20339  rrgsupp  20618  isdrngrd  20683  isdrngrdOLD  20685  nzerooringczr  21419  dsmmelbas  21678  dsmmacl  21680  frlmssuvc2  21734  mhpsclcl  22063  mhpmulcl  22065  elcls  22989  clsndisj  22991  elcls3  22999  neindisj2  23039  clslp  23064  cmpfi  23324  cmpfii  23325  dfconn2  23335  connsuba  23336  nconnsubb  23339  1stcelcls  23377  finlocfin  23436  locfincmp  23442  dissnlocfin  23445  locfindis  23446  ptclsg  23531  dfac14lem  23533  isfbas  23745  trfbas2  23759  isfil  23763  filss  23769  fbunfip  23785  fgval  23786  elfg  23787  isufil2  23824  ufileu  23835  filufint  23836  fmfnfm  23874  flimclslem  23900  fclsopni  23931  fclsnei  23935  fclsbas  23937  fclsrest  23940  fclscmp  23946  ufilcmp  23948  isfcf  23950  fcfnei  23951  fcfneii  23953  ptcmplem2  23969  cnextcn  23983  cnextfres1  23984  tsmsfbas  24044  iscusp  24214  cuspcvg  24216  lpbl  24419  prdsxmslem2  24445  restmetu  24486  qdensere  24685  lebnumlem3  24890  isphtpc  24921  iscmet  25212  cmetcvg  25213  equivcmet  25245  cmetcusp1  25281  cmetcusp  25282  rrxmvallem  25332  ovolicc2lem2  25447  ovolicc2lem5  25450  i1fres  25634  lhop1lem  25946  deg1ldg  26025  plyco0  26125  plyeq0lem  26143  coeeq2  26175  coe1termlem  26191  taylfval  26294  cxpeq0  26615  ftalem4  27014  ftalem5  27015  ftalem6  27016  isppw  27052  isnsqf  27073  sqff1o  27120  musum  27129  dchrelbas3  27177  dchrelbasd  27178  dchrelbas4  27182  dchrmulcl  27188  dchrn0  27189  dchrfi  27194  dchrptlem2  27204  dchrpt  27206  lgsne0  27274  lgsdchr  27294  2sqlem11  27368  nosupbnd2lem1  27655  expsne0  28360  ishlg  28581  uvtx01vtx  29377  pthdlem2lem  29747  2pthdlem1  29910  clwwlknclwwlkdif  29961  umgr2cwwkdifex  30047  3pthdlem1  30146  frgrregorufr  30307  numclwwlk2lem1lem  30324  numclwwlk2lem1  30358  numclwlk2lem2f  30359  numclwlk2lem2f1o  30361  nmorepnf  30750  nmoprepnf  31849  nmfnrepnf  31862  fdifsupp  32670  ressupprn  32675  disjdsct  32688  rmfsupp2  33212  domnprodn0  33249  isufd  33512  ufdprmidl  33513  1arithufdlem4  33519  dfufd2lem  33521  fedgmullem2  33664  constrconj  33779  constrelextdg2  33781  constrllcllem  33786  constrcbvlem  33789  locfinreflem  33874  sibfof  34374  signswch  34595  signstfvneq0  34606  vonf1owev  35173  derangenlem  35236  subfacp1lem3  35247  subfacp1lem5  35249  subfacp1lem6  35250  subfacp1  35251  iscvm  35324  cvmcov  35328  cvmcov2  35340  eldm3  35826  elima4  35841  neibastop1  36424  neibastop2lem  36425  neibastop2  36426  neibastop3  36427  neifg  36436  poimirlem17  37697  poimirlem18  37698  poimirlem20  37700  poimirlem21  37701  poimirlem22  37702  poimirlem23  37703  poimirlem27  37707  poimirlem28  37708  poimirlem30  37710  poimirlem31  37711  poimirlem32  37712  mblfinlem3  37719  itg2addnclem3  37733  sstotbnd2  37834  cntotbnd  37856  heibor1lem  37869  dmecd  38362  disjecxrn  38456  br1cosscnvxrn  38596  2llnm3N  39688  dalem4  39784  cdlemk28-3  41027  mapdh9a  41908  idomnnzpownz  42245  idomnnzgmulnz  42246  sticksstones1  42259  aks6d1c6lem1  42283  unitscyglem2  42309  unitscyglem3  42310  unitscyglem4  42311  readvcot  42482  domnexpgn0cl  42641  fsuppind  42708  dffltz  42752  pellexlem3  42948  mncn0  43256  aaitgo  43279  gneispace0nelrn2  44258  cvgdvgrat  44430  binomcxplemnotnn0  44473  disjf1  45304  disjrnmpt2  45309  disjinfi  45313  fsumiunss  45699  islptre  45743  islpcn  45761  lptre2pt  45762  0ellimcdiv  45771  liminflelimsup  45898  stoweidlem28  46150  stoweidlem43  46165  dirkercncflem2  46226  fourierdlem46  46274  fourierdlem79  46307  elaa2lem  46355  elaa2  46356  sge0fodjrnlem  46538  sge0iunmpt  46540  nnfoctbdjlem  46577  meadjiunlem  46587  meadjiun  46588  gpg5nbgrvtx13starlem1  48195  gpg5nbgrvtx13starlem3  48197  ovn0ssdmfun  48283  rmsupp0  48492  scmsuppss  48495  suppmptcfin  48500  linc1  48550  el0ldep  48591  ldepspr  48598  islindeps2  48608  zlmodzxzldeplem4  48628  zlmodzxzldep  48629  ldepsnlinclem1  48630  ldepsnlinclem2  48631  ldepsnlinc  48633  fvconstr  48986  fvconstrn0  48987  fvconstr2  48988  catprslem  49135  catprsc  49138  catprsc2  49139  oppccic  49169  relcic  49170  cicpropdlem  49174  secval  49872  cscval  49873  cotval  49874