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 ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ne 2957

This theorem is used by:  neeq2  3019  neeqtrd  3025  prneprprc  4821  fndifnfp  7173  f1ounsn  7272  f12dfv  7273  f13dfv  7274  resf1extb  7935  infpssrlem4  10365  sqrt2irr  16397  sdrgunit  21033  prmidlval  21598  dsmmval  22020  dsmmbas2  22023  frlmbas  22041  dfconn2  23717  alexsublem  24343  uc1pval  26438  mon1pval  26440  dchrsum2  27577  flt4ALT  27974  fltoprm  27977  noetainflem4  28079  isinag  29339  elcgrabasi  29357  uhgrwkspthlem2  30322  usgr2wlkneq  30324  usgr2trlspth  30329  lfgrn1cycl  30376  uspgrn2crct  30379  2pthdlem1  30501  3pthdlem1  30747  numclwwlk2lem1  30959  eigorth  32422  eighmorth  32548  mxidlval  33968  ressply1mon1p  34082  extdgfialglem1  34306  wlimeq12  36551  limsucncmpi  37203  mh-inf3f1  37299  poimirlem25  38531  poimirlem26  38532  pridlval  38935  maxidlval  38941  lshpset  40003  lduallkr3  40187  isatl  40324  cdlemk42  41966  prjspner1  43616  dffltz  43624  stoweidlem43  46997  nnfoctbdjlem  47409