Theorem neeq2d 3002

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ≠ wne 2941

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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  neeq2  3005  neeqtrd  3011  prneprprc  4862  fndifnfp  7174  f12dfv  7271  f13dfv  7272  infpssrlem4  10301  sqrt2irr  16192  sdrgunit  20412  dsmmval  21289  dsmmbas2  21292  frlmbas  21310  dfconn2  22923  alexsublem  23548  uc1pval  25657  mon1pval  25659  dchrsum2  26771  noetainflem4  27243  isinag  28089  uhgrwkspthlem2  29011  usgr2wlkneq  29013  usgr2trlspth  29018  lfgrn1cycl  29059  uspgrn2crct  29062  2pthdlem1  29184  3pthdlem1  29417  numclwwlk2lem1  29629  eigorth  31091  eighmorth  31217  prmidlval  32555  mxidlval  32577  ressply1mon1p  32657  wlimeq12  34791  limsucncmpi  35330  poimirlem25  36513  poimirlem26  36514  pridlval  36901  maxidlval  36907  lshpset  37848  lduallkr3  38032  isatl  38169  cdlemk42  39812  prjspner1  41368  dffltz  41376  stoweidlem43  44759  nnfoctbdjlem  45171