Theorem neeq2d 3007

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  neeq2  3010  neeqtrd  3016  prneprprc  4885  fndifnfp  7210  f12dfv  7309  f13dfv  7310  infpssrlem4  10375  sqrt2irr  16297  sdrgunit  20819  dsmmval  21777  dsmmbas2  21780  frlmbas  21798  dfconn2  23448  alexsublem  24073  uc1pval  26199  mon1pval  26201  dchrsum2  27330  noetainflem4  27803  isinag  28864  uhgrwkspthlem2  29790  usgr2wlkneq  29792  usgr2trlspth  29797  lfgrn1cycl  29838  uspgrn2crct  29841  2pthdlem1  29963  3pthdlem1  30196  numclwwlk2lem1  30408  eigorth  31870  eighmorth  31996  prmidlval  33430  mxidlval  33454  ressply1mon1p  33558  wlimeq12  35783  limsucncmpi  36411  poimirlem25  37605  poimirlem26  37606  pridlval  37993  maxidlval  37999  lshpset  38934  lduallkr3  39118  isatl  39255  cdlemk42  40898  prjspner1  42581  dffltz  42589  stoweidlem43  45964  nnfoctbdjlem  46376