Theorem neeq2d 3016

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  neeq2  3019  neeqtrd  3025  prneprprc  4818  fndifnfp  7156  f1ounsn  7252  f12dfv  7253  f13dfv  7254  resf1extb  7911  infpssrlem4  10260  sqrt2irr  16264  sdrgunit  20825  dsmmval  21766  dsmmbas2  21769  frlmbas  21787  dfconn2  23459  alexsublem  24084  uc1pval  26180  mon1pval  26182  dchrsum2  27309  noetainflem4  27781  isinag  28984  uhgrwkspthlem2  29900  usgr2wlkneq  29902  usgr2trlspth  29907  lfgrn1cycl  29951  uspgrn2crct  29954  2pthdlem1  30076  3pthdlem1  30312  numclwwlk2lem1  30524  eigorth  31987  eighmorth  32113  prmidlval  33584  mxidlval  33610  ressply1mon1p  33725  extdgfialglem1  33950  wlimeq12  36131  limsucncmpi  36769  poimirlem25  38108  poimirlem26  38109  pridlval  38496  maxidlval  38502  lshpset  39566  lduallkr3  39750  isatl  39887  cdlemk42  41529  prjspner1  43172  dffltz  43180  stoweidlem43  46581  nnfoctbdjlem  46993