Theorem neeq2d 3017

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ne 2958

This theorem is used by:  neeq2  3020  neeqtrd  3026  prneprprc  4824  fndifnfp  7178  f1ounsn  7277  f12dfv  7278  f13dfv  7279  resf1extb  7935  infpssrlem4  10312  sqrt2irr  16343  sdrgunit  20968  prmidlval  21531  dsmmval  21953  dsmmbas2  21956  frlmbas  21974  dfconn2  23650  alexsublem  24276  uc1pval  26372  mon1pval  26374  dchrsum2  27512  noetainflem4  27984  isinag  29244  elcgrabasi  29262  uhgrwkspthlem2  30227  usgr2wlkneq  30229  usgr2trlspth  30234  lfgrn1cycl  30281  uspgrn2crct  30284  2pthdlem1  30406  3pthdlem1  30652  numclwwlk2lem1  30864  eigorth  32327  eighmorth  32453  mxidlval  33872  ressply1mon1p  33986  extdgfialglem1  34210  wlimeq12  36404  limsucncmpi  37072  poimirlem25  38402  poimirlem26  38403  pridlval  38791  maxidlval  38797  lshpset  39859  lduallkr3  40043  isatl  40180  cdlemk42  41822  prjspner1  43480  dffltz  43488  stoweidlem43  46879  nnfoctbdjlem  47291