Theorem neeq2d 2992

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ne 2933

This theorem is referenced by:  neeq2  2995  neeqtrd  3001  prneprprc  4804  fndifnfp  7131  f1ounsn  7227  f12dfv  7228  f13dfv  7229  resf1extb  7885  infpssrlem4  10228  sqrt2irr  16216  sdrgunit  20773  dsmmval  21714  dsmmbas2  21717  frlmbas  21735  dfconn2  23384  alexsublem  24009  uc1pval  26105  mon1pval  26107  dchrsum2  27231  noetainflem4  27704  isinag  28906  uhgrwkspthlem2  29822  usgr2wlkneq  29824  usgr2trlspth  29829  lfgrn1cycl  29873  uspgrn2crct  29876  2pthdlem1  29998  3pthdlem1  30234  numclwwlk2lem1  30446  eigorth  31909  eighmorth  32035  prmidlval  33497  mxidlval  33521  ressply1mon1p  33628  extdgfialglem1  33836  wlimeq12  35999  limsucncmpi  36627  poimirlem25  37966  poimirlem26  37967  pridlval  38354  maxidlval  38360  lshpset  39424  lduallkr3  39608  isatl  39745  cdlemk42  41387  prjspner1  43059  dffltz  43067  stoweidlem43  46471  nnfoctbdjlem  46883