Theorem neeq2d 3047

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ≠ wne 2987

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-ne 2988

This theorem is referenced by:  neeq2  3050  neeqtrd  3056  prneprprc  4751  fndifnfp  6915  f12dfv  7008  f13dfv  7009  infpssrlem4  9717  sqrt2irr  15594  dsmmval  20423  dsmmbas2  20426  frlmbas  20444  dfconn2  22024  alexsublem  22649  uc1pval  24740  mon1pval  24742  dchrsum2  25852  isinag  26632  uhgrwkspthlem2  27543  usgr2wlkneq  27545  usgr2trlspth  27550  lfgrn1cycl  27591  uspgrn2crct  27594  2pthdlem1  27716  3pthdlem1  27949  numclwwlk2lem1  28161  eigorth  29621  eighmorth  29747  prmidlval  31020  mxidlval  31041  wlimeq12  33219  limsucncmpi  33906  poimirlem25  35082  poimirlem26  35083  pridlval  35471  maxidlval  35477  lshpset  36274  lduallkr3  36458  isatl  36595  cdlemk42  38237  dffltz  39615  stoweidlem43  42685  nnfoctbdjlem  43094