Theorem neeq2d 3000

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ≠ wne 2939

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-ne 2940

This theorem is referenced by:  neeq2  3003  neeqtrd  3009  prneprprc  4823  fndifnfp  7127  f12dfv  7224  f13dfv  7225  infpssrlem4  10251  sqrt2irr  16142  sdrgunit  20319  dsmmval  21177  dsmmbas2  21180  frlmbas  21198  dfconn2  22807  alexsublem  23432  uc1pval  25541  mon1pval  25543  dchrsum2  26653  noetainflem4  27125  isinag  27843  uhgrwkspthlem2  28765  usgr2wlkneq  28767  usgr2trlspth  28772  lfgrn1cycl  28813  uspgrn2crct  28816  2pthdlem1  28938  3pthdlem1  29171  numclwwlk2lem1  29383  eigorth  30843  eighmorth  30969  prmidlval  32285  mxidlval  32306  ressply1mon1p  32356  wlimeq12  34480  limsucncmpi  34993  poimirlem25  36176  poimirlem26  36177  pridlval  36565  maxidlval  36571  lshpset  37513  lduallkr3  37697  isatl  37834  cdlemk42  39477  prjspner1  41022  dffltz  41030  stoweidlem43  44404  nnfoctbdjlem  44816