Theorem neeq1d 2990

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ≠ wne 2930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-ne 2931

This theorem is referenced by:  neeq1  2993  eqnetrd  2998  inisegn0  6108  f12dfv  7287  f13dfv  7288  suppval1  8180  elsuppfng  8183  elsuppfn  8184  suppsnop  8192  ressuppss  8197  ressuppssdif  8199  tz7.49  8475  ereldm  8784  pw2f1olem  9114  marypha1lem  9476  wdomtr  9618  inf3lem2  9672  cantnflem1  9732  cantnf  9736  cplem2  9933  dfac9  10179  kmlem12  10204  infpssrlem4  10349  fin23lem14  10376  axcc2lem  10479  axcc3  10481  domtriomlem  10485  axdc2lem  10491  ac6c4  10524  zorn2lem6  10544  rpnnen1lem4  13016  rpnnen1lem5  13017  mptnn0fsuppr  14019  hashprg  14412  hashtpg  14504  prodfn0  15898  prodfrec  15899  prodfdiv  15900  ntrivcvgtail  15904  fproddiv  15963  fprodn0  15981  fproddivf  15989  dvdsle  16312  algcvg  16577  algcvga  16580  eucalgcvga  16587  rpdvds  16661  phibndlem  16772  dfphi2  16776  pcaddlem  16890  vdwmc  16980  iscatd2  17694  brcic  17814  cicer  17822  cat1lem  18118  cat1  18119  sgrp2nmndlem5  18919  symgextf1lem  19418  pmtrmvd  19454  frgpup3lem  19775  isirred  20401  rrgsupp  20679  isdrngrd  20744  isdrngrdOLD  20746  nzerooringczr  21470  dsmmelbas  21737  dsmmacl  21739  frlmssuvc2  21793  mhpsclcl  22141  mhpmulcl  22143  elcls  23068  clsndisj  23070  elcls3  23078  neindisj2  23118  clslp  23143  cmpfi  23403  cmpfii  23404  dfconn2  23414  connsuba  23415  nconnsubb  23418  1stcelcls  23456  finlocfin  23515  locfincmp  23521  dissnlocfin  23524  locfindis  23525  ptclsg  23610  dfac14lem  23612  isfbas  23824  trfbas2  23838  isfil  23842  filss  23848  fbunfip  23864  fgval  23865  elfg  23866  isufil2  23903  ufileu  23914  filufint  23915  fmfnfm  23953  flimclslem  23979  fclsopni  24010  fclsnei  24014  fclsbas  24016  fclsrest  24019  fclscmp  24025  ufilcmp  24027  isfcf  24029  fcfnei  24030  fcfneii  24032  ptcmplem2  24048  cnextcn  24062  cnextfres1  24063  tsmsfbas  24123  iscusp  24295  cuspcvg  24297  lpbl  24503  prdsxmslem2  24529  restmetu  24570  qdensere  24777  lebnumlem3  24980  isphtpc  25011  iscmet  25303  cmetcvg  25304  equivcmet  25336  cmetcusp1  25372  cmetcusp  25373  rrxmvallem  25423  ovolicc2lem2  25538  ovolicc2lem5  25541  i1fres  25726  lhop1lem  26037  deg1ldg  26119  plyco0  26219  plyeq0lem  26237  coeeq2  26269  coe1termlem  26285  taylfval  26386  cxpeq0  26705  ftalem4  27104  ftalem5  27105  ftalem6  27106  isppw  27142  isnsqf  27163  sqff1o  27210  musum  27219  dchrelbas3  27267  dchrelbasd  27268  dchrelbas4  27272  dchrmulcl  27278  dchrn0  27279  dchrfi  27284  dchrptlem2  27294  dchrpt  27296  lgsne0  27364  lgsdchr  27384  2sqlem11  27458  nosupbnd2lem1  27745  ishlg  28529  uvtx01vtx  29333  pthdlem2lem  29704  2pthdlem1  29864  clwwlknclwwlkdif  29912  umgr2cwwkdifex  29998  3pthdlem1  30097  frgrregorufr  30258  numclwwlk2lem1lem  30275  numclwwlk2lem1  30309  numclwlk2lem2f  30310  numclwlk2lem2f1o  30312  nmorepnf  30701  nmoprepnf  31800  nmfnrepnf  31813  ressupprn  32602  disjdsct  32614  rmfsupp2  33103  domnprodn0  33130  isufd  33415  ufdprmidl  33416  1arithufdlem4  33422  dfufd2lem  33424  fedgmullem2  33525  constrconj  33603  locfinreflem  33655  sibfof  34174  signswch  34407  signstfvneq0  34418  derangenlem  34999  subfacp1lem3  35010  subfacp1lem5  35012  subfacp1lem6  35013  subfacp1  35014  iscvm  35087  cvmcov  35091  cvmcov2  35103  eldm3  35583  elima4  35599  neibastop1  36071  neibastop2lem  36072  neibastop2  36073  neibastop3  36074  neifg  36083  poimirlem17  37338  poimirlem18  37339  poimirlem20  37341  poimirlem21  37342  poimirlem22  37343  poimirlem23  37344  poimirlem27  37348  poimirlem28  37349  poimirlem30  37351  poimirlem31  37352  poimirlem32  37353  mblfinlem3  37360  itg2addnclem3  37374  sstotbnd2  37475  cntotbnd  37497  heibor1lem  37510  dmecd  38002  disjecxrn  38087  br1cosscnvxrn  38172  2llnm3N  39268  dalem4  39364  cdlemk28-3  40607  mapdh9a  41488  idomnnzpownz  41830  idomnnzgmulnz  41831  sticksstones1  41844  aks6d1c6lem1  41868  metakunt29  41919  fsuppind  42062  dffltz  42288  pellexlem3  42488  mncn0  42800  aaitgo  42823  gneispace0nelrn2  43808  cvgdvgrat  43987  binomcxplemnotnn0  44030  disjf1  44790  disjrnmpt2  44795  disjinfi  44799  fsumiunss  45196  islptre  45240  islpcn  45260  lptre2pt  45261  0ellimcdiv  45270  liminflelimsup  45397  stoweidlem28  45649  stoweidlem43  45664  dirkercncflem2  45725  fourierdlem46  45773  fourierdlem79  45806  elaa2lem  45854  elaa2  45855  sge0fodjrnlem  46037  sge0iunmpt  46039  nnfoctbdjlem  46076  meadjiunlem  46086  meadjiun  46087  ovn0ssdmfun  47536  rmsupp0  47747  scmsuppss  47751  suppmptcfin  47758  linc1  47808  el0ldep  47849  ldepspr  47856  islindeps2  47866  zlmodzxzldeplem4  47886  zlmodzxzldep  47887  ldepsnlinclem1  47888  ldepsnlinclem2  47889  ldepsnlinc  47891  fvconstr  48223  fvconstrn0  48224  fvconstr2  48225  catprslem  48331  catprsc  48334  catprsc2  48335  secval  48493  cscval  48494  cotval  48495