Theorem neeq2d 3076

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ≠ wne 3016

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 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-ne 3017

This theorem is referenced by:  neeq2  3079  neeqtrd  3085  prneprprc  4791  fndifnfp  6938  f12dfv  7030  f13dfv  7031  infpssrlem4  9728  sqrt2irr  15602  dsmmval  20878  dsmmbas2  20881  frlmbas  20899  dfconn2  22027  alexsublem  22652  uc1pval  24733  mon1pval  24735  dchrsum2  25844  isinag  26624  uhgrwkspthlem2  27535  usgr2wlkneq  27537  usgr2trlspth  27542  lfgrn1cycl  27583  uspgrn2crct  27586  2pthdlem1  27709  3pthdlem1  27943  numclwwlk2lem1  28155  eigorth  29615  eighmorth  29741  prmidlval  30954  mxidlval  30970  wlimeq12  33106  limsucncmpi  33793  poimirlem25  34932  poimirlem26  34933  pridlval  35326  maxidlval  35332  lshpset  36129  lduallkr3  36313  isatl  36450  cdlemk42  38092  dffltz  39291  stoweidlem43  42348  nnfoctbdjlem  42757