Theorem neeq1d 2841

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  neeq1  2844  eqnetrd  2849  prnzgOLD  4255  inisegn0  5416  f12dfv  6429  f13dfv  6430  suppval1  7188  elsuppfn  7190  suppsnop  7196  ressuppss  7201  ressuppssdif  7203  tz7.49  7427  ereldm  7677  pw2f1olem  7949  marypha1lem  8222  wdomtr  8363  inf3lem2  8409  cantnflem1  8469  cantnf  8473  cplem2  8636  dfac9  8841  kmlem12  8866  infpssrlem4  9011  fin23lem14  9038  axcc2lem  9141  axcc3  9143  domtriomlem  9147  axdc2lem  9153  ac6c4  9186  zorn2lem6  9206  rpnnen1lem4  11693  rpnnen1lem5  11694  rpnnen1lem4OLD  11699  rpnnen1lem5OLD  11700  mptnn0fsuppr  12661  hashprg  13043  hashprgOLD  13044  hashtpg  13121  prodfn0  14465  prodfrec  14466  prodfdiv  14467  ntrivcvgtail  14471  fproddiv  14530  fprodn0  14548  fproddivf  14557  dvdsle  14870  algcvg  15127  algcvga  15130  eucalgcvga  15137  rpdvds  15212  phibndlem  15313  dfphi2  15317  pcaddlem  15430  vdwmc  15520  iscatd2  16165  brcic  16281  cicer  16289  sgrp2nmndlem5  17239  symgextf1lem  17663  pmtrmvd  17699  frgpup3lem  18013  isirred  18522  isdrngrd  18596  rrgsupp  19112  dsmmelbas  19902  dsmmacl  19904  frlmssuvc2  19953  elcls  20687  clsndisj  20689  elcls3  20697  neindisj2  20737  clslp  20762  cmpfi  21021  cmpfii  21022  dfcon2  21032  consuba  21033  nconsubb  21036  1stcelcls  21074  finlocfin  21133  locfincmp  21139  dissnlocfin  21142  locfindis  21143  ptclsg  21228  dfac14lem  21230  isfbas  21443  trfbas2  21457  isfil  21461  filss  21467  fbunfip  21483  fgval  21484  elfg  21485  isufil2  21522  ufileu  21533  filufint  21534  fmfnfm  21572  flimclslem  21598  fclsopni  21629  fclsnei  21633  fclsbas  21635  fclsrest  21638  fclscmp  21644  ufilcmp  21646  isfcf  21648  fcfnei  21649  fcfneii  21651  ptcmplem2  21667  cnextcn  21681  cnextfres1  21682  tsmsfbas  21741  iscusp  21913  cuspcvg  21915  lpbl  22118  prdsxmslem2  22144  restmetu  22185  qdensere  22383  lebnumlem3  22570  isphtpc  22601  iscmet  22890  cmetcvg  22891  equivcmet  22922  cmetcusp1  22957  cmetcusp  22958  rrxmvallem  22995  ovolicc2lem2  23093  ovolicc2lem5  23096  i1fres  23278  lhop1lem  23580  deg1ldg  23656  plyco0  23752  plyeq0lem  23770  coeeq2  23802  coe1termlem  23818  taylfval  23917  cxpeq0  24224  ftalem4  24602  ftalem5  24603  ftalem6  24604  isppw  24640  isnsqf  24661  sqff1o  24708  musum  24717  dchrelbas3  24763  dchrelbasd  24764  dchrelbas4  24768  dchrmulcl  24774  dchrn0  24775  dchrfi  24780  dchrptlem2  24790  dchrpt  24792  lgsne0  24860  lgsdchr  24880  2sqlem11  24954  ishlg  25297  uvtx01vtx  26020  usg2cwwkdifex  26349  frgraregorufr  26580  clwwlkextfrlem1  26603  numclwwlkovh  26628  numclwwlk2lem1  26629  numclwlk2lem2f  26630  numclwlk2lem2f1o  26632  numclwwlk5  26639  nmorepnf  27007  nmoprepnf  28110  nmfnrepnf  28123  disjdsct  28863  locfinreflem  29235  sibfof  29729  signswch  29964  signstfvneq0  29975  derangenlem  30407  subfacp1lem3  30418  subfacp1lem5  30420  subfacp1lem6  30421  subfacp1  30422  iscvm  30495  cvmcov  30499  cvmcov2  30511  eldm3  30905  elima4  30924  nobndlem2  31092  nobndlem4  31094  nobndlem5  31095  nobndlem6  31096  nobndlem8  31098  nobndup  31099  nobnddown  31100  nofulllem5  31105  neibastop1  31524  neibastop2lem  31525  neibastop2  31526  neibastop3  31527  neifg  31536  poimirlem17  32596  poimirlem18  32597  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem27  32606  poimirlem28  32607  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  mblfinlem3  32618  itg2addnclem3  32633  sstotbnd2  32743  cntotbnd  32765  heibor1lem  32778  2llnm3N  33873  dalem4  33969  cdlemk28-3  35214  mapdh9a  36097  pellexlem3  36413  mncn0  36728  aaitgo  36751  gneispace0nelrn2  37459  cvgdvgrat  37534  binomcxplemnotnn0  37577  disjf1  38364  disjrnmpt2  38370  disjinfi  38375  fsumiunss  38642  islptre  38686  islpcn  38706  lptre2pt  38707  0ellimcdiv  38716  stoweidlem28  38921  stoweidlem43  38936  dirkercncflem2  38997  fourierdlem46  39045  fourierdlem79  39078  elaa2lem  39126  elaa2  39127  sge0fodjrnlem  39309  sge0iunmpt  39311  nnfoctbdjlem  39348  meadjiunlem  39358  meadjiun  39359  uvtxa01vtx0  40623  pthdlem2lem  40973  2pthdlem1  41137  umgr2cwwkdifex  41249  clwlksfclwwlk  41269  3pthdlem1  41331  frgrregorufr  41490  av-clwwlkextfrlem1  41509  av-numclwwlkovh  41531  av-numclwwlk2lem1  41532  av-numclwlk2lem2f  41533  av-numclwlk2lem2f1o  41535  av-numclwwlk5  41542  ovn0ssdmfun  41557  nzerooringczr  41864  rmsupp0  41943  scmsuppss  41947  suppmptcfin  41954  linc1  42008  el0ldep  42049  ldepspr  42056  islindeps2  42066  zlmodzxzldeplem4  42086  zlmodzxzldep  42087  ldepsnlinclem1  42088  ldepsnlinclem2  42089  ldepsnlinc  42091  secval  42287  cscval  42288  cotval  42289