Theorem neeq2d 3020

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ≠ wne 2960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ne 2961

This theorem is referenced by:  neeq2  3023  neeqtrd  3029  prneprprc  4822  fndifnfp  7164  f1ounsn  7260  f12dfv  7261  f13dfv  7262  resf1extb  7919  infpssrlem4  10278  sqrt2irr  16295  sdrgunit  20868  prmidlval  21424  dsmmval  21844  dsmmbas2  21847  frlmbas  21865  dfconn2  23537  alexsublem  24162  uc1pval  26258  mon1pval  26260  dchrsum2  27390  noetainflem4  27862  isinag  29090  uhgrwkspthlem2  30012  usgr2wlkneq  30014  usgr2trlspth  30019  lfgrn1cycl  30063  uspgrn2crct  30066  2pthdlem1  30188  3pthdlem1  30424  numclwwlk2lem1  30636  eigorth  32099  eighmorth  32225  mxidlval  33661  ressply1mon1p  33775  extdgfialglem1  33999  wlimeq12  36180  limsucncmpi  36818  poimirlem25  38156  poimirlem26  38157  pridlval  38544  maxidlval  38550  lshpset  39614  lduallkr3  39798  isatl  39935  cdlemk42  41577  prjspner1  43220  dffltz  43228  stoweidlem43  46615  nnfoctbdjlem  47027