Theorem neeq1d 3006

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  neeq1  3009  eqnetrd  3014  inisegn0  6128  f12dfv  7309  f13dfv  7310  suppval1  8207  elsuppfng  8210  elsuppfn  8211  suppsnop  8219  ressuppss  8224  ressuppssdif  8226  tz7.49  8501  ereldm  8813  pw2f1olem  9142  marypha1lem  9502  wdomtr  9644  inf3lem2  9698  cantnflem1  9758  cantnf  9762  cplem2  9959  dfac9  10206  kmlem12  10231  infpssrlem4  10375  fin23lem14  10402  axcc2lem  10505  axcc3  10507  domtriomlem  10511  axdc2lem  10517  ac6c4  10550  zorn2lem6  10570  rpnnen1lem4  13045  rpnnen1lem5  13046  mptnn0fsuppr  14050  hashprg  14444  hashtpg  14534  prodfn0  15942  prodfrec  15943  prodfdiv  15944  ntrivcvgtail  15948  fproddiv  16009  fprodn0  16027  fproddivf  16035  dvdsle  16358  algcvg  16623  algcvga  16626  eucalgcvga  16633  rpdvds  16707  phibndlem  16817  dfphi2  16821  pcaddlem  16935  vdwmc  17025  iscatd2  17739  brcic  17859  cicer  17867  cat1lem  18163  cat1  18164  sgrp2nmndlem5  18964  symgextf1lem  19462  pmtrmvd  19498  frgpup3lem  19819  isirred  20445  rrgsupp  20723  isdrngrd  20788  isdrngrdOLD  20790  nzerooringczr  21514  dsmmelbas  21782  dsmmacl  21784  frlmssuvc2  21838  mhpsclcl  22174  mhpmulcl  22176  elcls  23102  clsndisj  23104  elcls3  23112  neindisj2  23152  clslp  23177  cmpfi  23437  cmpfii  23438  dfconn2  23448  connsuba  23449  nconnsubb  23452  1stcelcls  23490  finlocfin  23549  locfincmp  23555  dissnlocfin  23558  locfindis  23559  ptclsg  23644  dfac14lem  23646  isfbas  23858  trfbas2  23872  isfil  23876  filss  23882  fbunfip  23898  fgval  23899  elfg  23900  isufil2  23937  ufileu  23948  filufint  23949  fmfnfm  23987  flimclslem  24013  fclsopni  24044  fclsnei  24048  fclsbas  24050  fclsrest  24053  fclscmp  24059  ufilcmp  24061  isfcf  24063  fcfnei  24064  fcfneii  24066  ptcmplem2  24082  cnextcn  24096  cnextfres1  24097  tsmsfbas  24157  iscusp  24329  cuspcvg  24331  lpbl  24537  prdsxmslem2  24563  restmetu  24604  qdensere  24811  lebnumlem3  25014  isphtpc  25045  iscmet  25337  cmetcvg  25338  equivcmet  25370  cmetcusp1  25406  cmetcusp  25407  rrxmvallem  25457  ovolicc2lem2  25572  ovolicc2lem5  25575  i1fres  25760  lhop1lem  26072  deg1ldg  26151  plyco0  26251  plyeq0lem  26269  coeeq2  26301  coe1termlem  26317  taylfval  26418  cxpeq0  26738  ftalem4  27137  ftalem5  27138  ftalem6  27139  isppw  27175  isnsqf  27196  sqff1o  27243  musum  27252  dchrelbas3  27300  dchrelbasd  27301  dchrelbas4  27305  dchrmulcl  27311  dchrn0  27312  dchrfi  27317  dchrptlem2  27327  dchrpt  27329  lgsne0  27397  lgsdchr  27417  2sqlem11  27491  nosupbnd2lem1  27778  expsne0  28432  ishlg  28628  uvtx01vtx  29432  pthdlem2lem  29803  2pthdlem1  29963  clwwlknclwwlkdif  30011  umgr2cwwkdifex  30097  3pthdlem1  30196  frgrregorufr  30357  numclwwlk2lem1lem  30374  numclwwlk2lem1  30408  numclwlk2lem2f  30409  numclwlk2lem2f1o  30411  nmorepnf  30800  nmoprepnf  31899  nmfnrepnf  31912  ressupprn  32702  disjdsct  32714  rmfsupp2  33218  domnprodn0  33247  isufd  33533  ufdprmidl  33534  1arithufdlem4  33540  dfufd2lem  33542  fedgmullem2  33643  constrconj  33735  constrelextdg2  33737  locfinreflem  33786  sibfof  34305  signswch  34538  signstfvneq0  34549  derangenlem  35139  subfacp1lem3  35150  subfacp1lem5  35152  subfacp1lem6  35153  subfacp1  35154  iscvm  35227  cvmcov  35231  cvmcov2  35243  eldm3  35723  elima4  35739  neibastop1  36325  neibastop2lem  36326  neibastop2  36327  neibastop3  36328  neifg  36337  poimirlem17  37597  poimirlem18  37598  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem27  37607  poimirlem28  37608  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  mblfinlem3  37619  itg2addnclem3  37633  sstotbnd2  37734  cntotbnd  37756  heibor1lem  37769  dmecd  38260  disjecxrn  38345  br1cosscnvxrn  38430  2llnm3N  39526  dalem4  39622  cdlemk28-3  40865  mapdh9a  41746  idomnnzpownz  42089  idomnnzgmulnz  42090  sticksstones1  42103  aks6d1c6lem1  42127  unitscyglem2  42153  unitscyglem3  42154  unitscyglem4  42155  metakunt29  42190  domnexpgn0cl  42478  fsuppind  42545  dffltz  42589  pellexlem3  42787  mncn0  43096  aaitgo  43119  gneispace0nelrn2  44103  cvgdvgrat  44282  binomcxplemnotnn0  44325  disjf1  45090  disjrnmpt2  45095  disjinfi  45099  fsumiunss  45496  islptre  45540  islpcn  45560  lptre2pt  45561  0ellimcdiv  45570  liminflelimsup  45697  stoweidlem28  45949  stoweidlem43  45964  dirkercncflem2  46025  fourierdlem46  46073  fourierdlem79  46106  elaa2lem  46154  elaa2  46155  sge0fodjrnlem  46337  sge0iunmpt  46339  nnfoctbdjlem  46376  meadjiunlem  46386  meadjiun  46387  ovn0ssdmfun  47882  rmsupp0  48093  scmsuppss  48097  suppmptcfin  48104  linc1  48154  el0ldep  48195  ldepspr  48202  islindeps2  48212  zlmodzxzldeplem4  48232  zlmodzxzldep  48233  ldepsnlinclem1  48234  ldepsnlinclem2  48235  ldepsnlinc  48237  fvconstr  48569  fvconstrn0  48570  fvconstr2  48571  catprslem  48677  catprsc  48680  catprsc2  48681  secval  48839  cscval  48840  cotval  48841