Theorem neeq1d 2984

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  neeq1  2987  eqnetrd  2992  iftrueb  4491  inisegn0  6053  f1ounsn  7213  f12dfv  7214  f13dfv  7215  resf1extb  7874  suppval1  8106  elsuppfng  8109  elsuppfn  8110  suppsnop  8118  ressuppss  8123  ressuppssdif  8125  tz7.49  8374  ereldm  8685  pw2f1olem  9005  marypha1lem  9342  wdomtr  9486  inf3lem2  9544  cantnflem1  9604  cantnf  9608  cplem2  9805  dfac9  10050  kmlem12  10075  infpssrlem4  10219  fin23lem14  10246  axcc2lem  10349  axcc3  10351  domtriomlem  10355  axdc2lem  10361  ac6c4  10394  zorn2lem6  10414  rpnnen1lem4  12899  rpnnen1lem5  12900  mptnn0fsuppr  13924  hashprg  14320  hashtpg  14410  prodfn0  15819  prodfrec  15820  prodfdiv  15821  ntrivcvgtail  15825  fproddiv  15886  fprodn0  15904  fproddivf  15912  dvdsle  16239  algcvg  16505  algcvga  16508  eucalgcvga  16515  rpdvds  16589  phibndlem  16699  dfphi2  16703  pcaddlem  16818  vdwmc  16908  iscatd2  17605  brcic  17723  cicer  17731  cat1lem  18021  cat1  18022  sgrp2nmndlem5  18821  symgextf1lem  19317  pmtrmvd  19353  frgpup3lem  19674  isirred  20322  rrgsupp  20604  isdrngrd  20669  isdrngrdOLD  20671  nzerooringczr  21405  dsmmelbas  21664  dsmmacl  21666  frlmssuvc2  21720  mhpsclcl  22050  mhpmulcl  22052  elcls  22976  clsndisj  22978  elcls3  22986  neindisj2  23026  clslp  23051  cmpfi  23311  cmpfii  23312  dfconn2  23322  connsuba  23323  nconnsubb  23326  1stcelcls  23364  finlocfin  23423  locfincmp  23429  dissnlocfin  23432  locfindis  23433  ptclsg  23518  dfac14lem  23520  isfbas  23732  trfbas2  23746  isfil  23750  filss  23756  fbunfip  23772  fgval  23773  elfg  23774  isufil2  23811  ufileu  23822  filufint  23823  fmfnfm  23861  flimclslem  23887  fclsopni  23918  fclsnei  23922  fclsbas  23924  fclsrest  23927  fclscmp  23933  ufilcmp  23935  isfcf  23937  fcfnei  23938  fcfneii  23940  ptcmplem2  23956  cnextcn  23970  cnextfres1  23971  tsmsfbas  24031  iscusp  24202  cuspcvg  24204  lpbl  24407  prdsxmslem2  24433  restmetu  24474  qdensere  24673  lebnumlem3  24878  isphtpc  24909  iscmet  25200  cmetcvg  25201  equivcmet  25233  cmetcusp1  25269  cmetcusp  25270  rrxmvallem  25320  ovolicc2lem2  25435  ovolicc2lem5  25438  i1fres  25622  lhop1lem  25934  deg1ldg  26013  plyco0  26113  plyeq0lem  26131  coeeq2  26163  coe1termlem  26179  taylfval  26282  cxpeq0  26603  ftalem4  27002  ftalem5  27003  ftalem6  27004  isppw  27040  isnsqf  27061  sqff1o  27108  musum  27117  dchrelbas3  27165  dchrelbasd  27166  dchrelbas4  27170  dchrmulcl  27176  dchrn0  27177  dchrfi  27182  dchrptlem2  27192  dchrpt  27194  lgsne0  27262  lgsdchr  27282  2sqlem11  27356  nosupbnd2lem1  27643  expsne0  28346  ishlg  28565  uvtx01vtx  29360  pthdlem2lem  29730  2pthdlem1  29893  clwwlknclwwlkdif  29941  umgr2cwwkdifex  30027  3pthdlem1  30126  frgrregorufr  30287  numclwwlk2lem1lem  30304  numclwwlk2lem1  30338  numclwlk2lem2f  30339  numclwlk2lem2f1o  30341  nmorepnf  30730  nmoprepnf  31829  nmfnrepnf  31842  fdifsupp  32641  ressupprn  32646  disjdsct  32659  rmfsupp2  33188  domnprodn0  33225  isufd  33487  ufdprmidl  33488  1arithufdlem4  33494  dfufd2lem  33496  fedgmullem2  33602  constrconj  33711  constrelextdg2  33713  constrllcllem  33718  constrcbvlem  33721  locfinreflem  33806  sibfof  34307  signswch  34528  signstfvneq0  34539  vonf1owev  35080  derangenlem  35143  subfacp1lem3  35154  subfacp1lem5  35156  subfacp1lem6  35157  subfacp1  35158  iscvm  35231  cvmcov  35235  cvmcov2  35247  eldm3  35733  elima4  35748  neibastop1  36332  neibastop2lem  36333  neibastop2  36334  neibastop3  36335  neifg  36344  poimirlem17  37616  poimirlem18  37617  poimirlem20  37619  poimirlem21  37620  poimirlem22  37621  poimirlem23  37622  poimirlem27  37626  poimirlem28  37627  poimirlem30  37629  poimirlem31  37630  poimirlem32  37631  mblfinlem3  37638  itg2addnclem3  37652  sstotbnd2  37753  cntotbnd  37775  heibor1lem  37788  dmecd  38277  disjecxrn  38360  br1cosscnvxrn  38450  2llnm3N  39548  dalem4  39644  cdlemk28-3  40887  mapdh9a  41768  idomnnzpownz  42105  idomnnzgmulnz  42106  sticksstones1  42119  aks6d1c6lem1  42143  unitscyglem2  42169  unitscyglem3  42170  unitscyglem4  42171  readvcot  42337  domnexpgn0cl  42496  fsuppind  42563  dffltz  42607  pellexlem3  42804  mncn0  43112  aaitgo  43135  gneispace0nelrn2  44114  cvgdvgrat  44286  binomcxplemnotnn0  44329  disjf1  45161  disjrnmpt2  45166  disjinfi  45170  fsumiunss  45557  islptre  45601  islpcn  45621  lptre2pt  45622  0ellimcdiv  45631  liminflelimsup  45758  stoweidlem28  46010  stoweidlem43  46025  dirkercncflem2  46086  fourierdlem46  46134  fourierdlem79  46167  elaa2lem  46215  elaa2  46216  sge0fodjrnlem  46398  sge0iunmpt  46400  nnfoctbdjlem  46437  meadjiunlem  46447  meadjiun  46448  gpg5nbgrvtx13starlem1  48056  gpg5nbgrvtx13starlem3  48058  ovn0ssdmfun  48144  rmsupp0  48353  scmsuppss  48356  suppmptcfin  48361  linc1  48411  el0ldep  48452  ldepspr  48459  islindeps2  48469  zlmodzxzldeplem4  48489  zlmodzxzldep  48490  ldepsnlinclem1  48491  ldepsnlinclem2  48492  ldepsnlinc  48494  fvconstr  48847  fvconstrn0  48848  fvconstr2  48849  catprslem  48996  catprsc  48999  catprsc2  49000  oppccic  49030  relcic  49031  cicpropdlem  49035  secval  49733  cscval  49734  cotval  49735