Theorem neeq2d 3003

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 2749	. 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:  neeq2  3006  neeqtrd  3012  prneprprc  4788  fndifnfp  7030  f12dfv  7126  f13dfv  7127  infpssrlem4  9993  sqrt2irr  15886  dsmmval  20851  dsmmbas2  20854  frlmbas  20872  dfconn2  22478  alexsublem  23103  uc1pval  25209  mon1pval  25211  dchrsum2  26321  isinag  27103  uhgrwkspthlem2  28023  usgr2wlkneq  28025  usgr2trlspth  28030  lfgrn1cycl  28071  uspgrn2crct  28074  2pthdlem1  28196  3pthdlem1  28429  numclwwlk2lem1  28641  eigorth  30101  eighmorth  30227  prmidlval  31514  mxidlval  31535  wlimeq12  33740  noetainflem4  33870  limsucncmpi  34561  poimirlem25  35729  poimirlem26  35730  pridlval  36118  maxidlval  36124  lshpset  36919  lduallkr3  37103  isatl  37240  cdlemk42  38882  prjspner1  40384  dffltz  40387  stoweidlem43  43474  nnfoctbdjlem  43883