Theorem neeq2d 3004

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ne 2944

This theorem is referenced by:  neeq2  3007  neeqtrd  3013  prneprprc  4791  fndifnfp  7048  f12dfv  7145  f13dfv  7146  infpssrlem4  10062  sqrt2irr  15958  dsmmval  20941  dsmmbas2  20944  frlmbas  20962  dfconn2  22570  alexsublem  23195  uc1pval  25304  mon1pval  25306  dchrsum2  26416  isinag  27199  uhgrwkspthlem2  28122  usgr2wlkneq  28124  usgr2trlspth  28129  lfgrn1cycl  28170  uspgrn2crct  28173  2pthdlem1  28295  3pthdlem1  28528  numclwwlk2lem1  28740  eigorth  30200  eighmorth  30326  prmidlval  31612  mxidlval  31633  wlimeq12  33813  noetainflem4  33943  limsucncmpi  34634  poimirlem25  35802  poimirlem26  35803  pridlval  36191  maxidlval  36197  lshpset  36992  lduallkr3  37176  isatl  37313  cdlemk42  38955  prjspner1  40463  dffltz  40471  stoweidlem43  43584  nnfoctbdjlem  43993