Theorem neeq2d 2985

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  neeq2  2988  neeqtrd  2994  prneprprc  4815  fndifnfp  7116  f1ounsn  7213  f12dfv  7214  f13dfv  7215  resf1extb  7874  infpssrlem4  10219  sqrt2irr  16176  sdrgunit  20699  dsmmval  21659  dsmmbas2  21662  frlmbas  21680  dfconn2  23322  alexsublem  23947  uc1pval  26061  mon1pval  26063  dchrsum2  27195  noetainflem4  27668  isinag  28801  uhgrwkspthlem2  29717  usgr2wlkneq  29719  usgr2trlspth  29724  lfgrn1cycl  29768  uspgrn2crct  29771  2pthdlem1  29893  3pthdlem1  30126  numclwwlk2lem1  30338  eigorth  31800  eighmorth  31926  prmidlval  33384  mxidlval  33408  ressply1mon1p  33513  wlimeq12  35792  limsucncmpi  36418  poimirlem25  37624  poimirlem26  37625  pridlval  38012  maxidlval  38018  lshpset  38956  lduallkr3  39140  isatl  39277  cdlemk42  40920  prjspner1  42599  dffltz  42607  stoweidlem43  46025  nnfoctbdjlem  46437