Theorem neeq1d 3002

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ≠ wne 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  neeq1  3005  eqnetrd  3010  inisegn0  5995  f12dfv  7126  f13dfv  7127  suppval1  7954  elsuppfng  7957  elsuppfn  7958  suppsnop  7965  ressuppss  7970  ressuppssdif  7972  tz7.49  8246  ereldm  8504  pw2f1olem  8816  marypha1lem  9122  wdomtr  9264  inf3lem2  9317  cantnflem1  9377  cantnf  9381  cplem2  9579  dfac9  9823  kmlem12  9848  infpssrlem4  9993  fin23lem14  10020  axcc2lem  10123  axcc3  10125  domtriomlem  10129  axdc2lem  10135  ac6c4  10168  zorn2lem6  10188  rpnnen1lem4  12649  rpnnen1lem5  12650  mptnn0fsuppr  13647  hashprg  14038  hashtpg  14127  prodfn0  15534  prodfrec  15535  prodfdiv  15536  ntrivcvgtail  15540  fproddiv  15599  fprodn0  15617  fproddivf  15625  dvdsle  15947  algcvg  16209  algcvga  16212  eucalgcvga  16219  rpdvds  16293  phibndlem  16399  dfphi2  16403  pcaddlem  16517  vdwmc  16607  iscatd2  17307  brcic  17427  cicer  17435  cat1lem  17727  cat1  17728  sgrp2nmndlem5  18483  symgextf1lem  18943  pmtrmvd  18979  frgpup3lem  19298  isirred  19856  isdrngrd  19932  rrgsupp  20475  dsmmelbas  20856  dsmmacl  20858  frlmssuvc2  20912  mhpsclcl  21247  mhpmulcl  21249  elcls  22132  clsndisj  22134  elcls3  22142  neindisj2  22182  clslp  22207  cmpfi  22467  cmpfii  22468  dfconn2  22478  connsuba  22479  nconnsubb  22482  1stcelcls  22520  finlocfin  22579  locfincmp  22585  dissnlocfin  22588  locfindis  22589  ptclsg  22674  dfac14lem  22676  isfbas  22888  trfbas2  22902  isfil  22906  filss  22912  fbunfip  22928  fgval  22929  elfg  22930  isufil2  22967  ufileu  22978  filufint  22979  fmfnfm  23017  flimclslem  23043  fclsopni  23074  fclsnei  23078  fclsbas  23080  fclsrest  23083  fclscmp  23089  ufilcmp  23091  isfcf  23093  fcfnei  23094  fcfneii  23096  ptcmplem2  23112  cnextcn  23126  cnextfres1  23127  tsmsfbas  23187  iscusp  23359  cuspcvg  23361  lpbl  23565  prdsxmslem2  23591  restmetu  23632  qdensere  23839  lebnumlem3  24032  isphtpc  24063  iscmet  24353  cmetcvg  24354  equivcmet  24386  cmetcusp1  24422  cmetcusp  24423  rrxmvallem  24473  ovolicc2lem2  24587  ovolicc2lem5  24590  i1fres  24775  lhop1lem  25082  deg1ldg  25162  plyco0  25258  plyeq0lem  25276  coeeq2  25308  coe1termlem  25324  taylfval  25423  cxpeq0  25738  ftalem4  26130  ftalem5  26131  ftalem6  26132  isppw  26168  isnsqf  26189  sqff1o  26236  musum  26245  dchrelbas3  26291  dchrelbasd  26292  dchrelbas4  26296  dchrmulcl  26302  dchrn0  26303  dchrfi  26308  dchrptlem2  26318  dchrpt  26320  lgsne0  26388  lgsdchr  26408  2sqlem11  26482  ishlg  26867  uvtx01vtx  27667  pthdlem2lem  28036  2pthdlem1  28196  clwwlknclwwlkdif  28244  umgr2cwwkdifex  28330  3pthdlem1  28429  frgrregorufr  28590  numclwwlk2lem1lem  28607  numclwwlk2lem1  28641  numclwlk2lem2f  28642  numclwlk2lem2f1o  28644  nmorepnf  29031  nmoprepnf  30130  nmfnrepnf  30143  ressupprn  30926  disjdsct  30937  rmfsupp2  31394  isufd  31565  fedgmullem2  31613  locfinreflem  31692  sibfof  32207  signswch  32440  signstfvneq0  32451  derangenlem  33033  subfacp1lem3  33044  subfacp1lem5  33046  subfacp1lem6  33047  subfacp1  33048  iscvm  33121  cvmcov  33125  cvmcov2  33137  eldm3  33634  elima4  33656  nosupbnd2lem1  33845  neibastop1  34475  neibastop2lem  34476  neibastop2  34477  neibastop3  34478  neifg  34487  poimirlem17  35721  poimirlem18  35722  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem23  35727  poimirlem27  35731  poimirlem28  35732  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  mblfinlem3  35743  itg2addnclem3  35757  sstotbnd2  35859  cntotbnd  35881  heibor1lem  35894  dmecd  36367  br1cosscnvxrn  36519  2llnm3N  37510  dalem4  37606  cdlemk28-3  38849  mapdh9a  39730  sticksstones1  40030  metakunt29  40081  fsuppind  40202  dffltz  40387  pellexlem3  40569  mncn0  40880  aaitgo  40903  gneispace0nelrn2  41640  cvgdvgrat  41820  binomcxplemnotnn0  41863  disjf1  42609  disjrnmpt2  42615  disjinfi  42620  fsumiunss  43006  islptre  43050  islpcn  43070  lptre2pt  43071  0ellimcdiv  43080  liminflelimsup  43207  stoweidlem28  43459  stoweidlem43  43474  dirkercncflem2  43535  fourierdlem46  43583  fourierdlem79  43616  elaa2lem  43664  elaa2  43665  sge0fodjrnlem  43844  sge0iunmpt  43846  nnfoctbdjlem  43883  meadjiunlem  43893  meadjiun  43894  ovn0ssdmfun  45209  nzerooringczr  45518  rmsupp0  45592  scmsuppss  45596  suppmptcfin  45603  linc1  45654  el0ldep  45695  ldepspr  45702  islindeps2  45712  zlmodzxzldeplem4  45732  zlmodzxzldep  45733  ldepsnlinclem1  45734  ldepsnlinclem2  45735  ldepsnlinc  45737  fvconstr  46071  fvconstrn0  46072  fvconstr2  46073  catprslem  46179  catprsc  46182  catprsc2  46183  secval  46335  cscval  46336  cotval  46337