Theorem neeq2d 3000

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
neeq2d	⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))

Proof of Theorem neeq2d

Step	Hyp	Ref	Expression
1		neeq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqeq2d 2742	. 2 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
3	2	necon3bid 2984	1 ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ≠ wne 2939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2940

This theorem is referenced by:  neeq2  3003  neeqtrd  3009  prneprprc  4861  fndifnfp  7176  f12dfv  7274  f13dfv  7275  infpssrlem4  10307  sqrt2irr  16199  sdrgunit  20643  dsmmval  21599  dsmmbas2  21602  frlmbas  21620  dfconn2  23243  alexsublem  23868  uc1pval  25995  mon1pval  25997  dchrsum2  27115  noetainflem4  27587  isinag  28523  uhgrwkspthlem2  29445  usgr2wlkneq  29447  usgr2trlspth  29452  lfgrn1cycl  29493  uspgrn2crct  29496  2pthdlem1  29618  3pthdlem1  29851  numclwwlk2lem1  30063  eigorth  31525  eighmorth  31651  prmidlval  32996  mxidlval  33018  ressply1mon1p  33098  wlimeq12  35262  limsucncmpi  35796  poimirlem25  36979  poimirlem26  36980  pridlval  37367  maxidlval  37373  lshpset  38314  lduallkr3  38498  isatl  38635  cdlemk42  40278  prjspner1  41833  dffltz  41841  stoweidlem43  45220  nnfoctbdjlem  45632