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 1541   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  neeq2  2995  neeqtrd  3001  prneprprc  4817  fndifnfp  7122  f1ounsn  7218  f12dfv  7219  f13dfv  7220  resf1extb  7876  infpssrlem4  10216  sqrt2irr  16174  sdrgunit  20729  dsmmval  21689  dsmmbas2  21692  frlmbas  21710  dfconn2  23363  alexsublem  23988  uc1pval  26101  mon1pval  26103  dchrsum2  27235  noetainflem4  27708  isinag  28910  uhgrwkspthlem2  29827  usgr2wlkneq  29829  usgr2trlspth  29834  lfgrn1cycl  29878  uspgrn2crct  29881  2pthdlem1  30003  3pthdlem1  30239  numclwwlk2lem1  30451  eigorth  31913  eighmorth  32039  prmidlval  33518  mxidlval  33542  ressply1mon1p  33649  extdgfialglem1  33849  wlimeq12  36011  limsucncmpi  36639  poimirlem25  37842  poimirlem26  37843  pridlval  38230  maxidlval  38236  lshpset  39234  lduallkr3  39418  isatl  39555  cdlemk42  41197  prjspner1  42865  dffltz  42873  stoweidlem43  46283  nnfoctbdjlem  46695