Theorem neeq2d 3018

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  neeq2  3021  neeqtrd  3027  prneprprc  4827  fndifnfp  7176  f1ounsn  7272  f12dfv  7273  f13dfv  7274  resf1extb  7932  infpssrlem4  10291  sqrt2irr  16306  sdrgunit  20880  prmidlval  21443  dsmmval  21865  dsmmbas2  21868  frlmbas  21886  dfconn2  23557  alexsublem  24182  uc1pval  26278  mon1pval  26280  dchrsum2  27410  noetainflem4  27882  isinag  29133  uhgrwkspthlem2  30081  usgr2wlkneq  30083  usgr2trlspth  30088  lfgrn1cycl  30132  uspgrn2crct  30135  2pthdlem1  30257  3pthdlem1  30493  numclwwlk2lem1  30705  eigorth  32168  eighmorth  32294  mxidlval  33722  ressply1mon1p  33836  extdgfialglem1  34060  wlimeq12  36287  limsucncmpi  36934  poimirlem25  38274  poimirlem26  38275  pridlval  38662  maxidlval  38668  lshpset  39730  lduallkr3  39914  isatl  40051  cdlemk42  41693  prjspner1  43338  dffltz  43346  stoweidlem43  46737  nnfoctbdjlem  47149