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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1631   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-ne 2944

This theorem is referenced by:  neeq2  3006  neeqtrd  3012  prneprprc  4526  fndifnfp  6586  f12dfv  6672  f13dfv  6673  infpssrlem4  9330  sqrt2irr  15185  dsmmval  20295  dsmmbas2  20298  frlmbas  20316  dfconn2  21443  alexsublem  22068  uc1pval  24119  mon1pval  24121  dchrsum2  25214  isinag  25950  uhgrwkspthlem2  26885  usgr2wlkneq  26887  usgr2trlspth  26892  lfgrn1cycl  26933  uspgrn2crct  26936  2pthdlem1  27077  3pthdlem1  27344  numclwwlk2lem1  27567  numclwwlk2lem1OLD  27574  eigorth  29037  eighmorth  29163  wlimeq12  32101  limsucncmpi  32781  poimirlem25  33767  poimirlem26  33768  pridlval  34164  maxidlval  34170  lshpset  34787  lduallkr3  34971  isatl  35108  cdlemk42  36750  stoweidlem43  40777  nnfoctbdjlem  41189