Theorem neeq2d 3015

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956

This theorem is used by:  neeq2  3018  neeqtrd  3024  prneprprc  4815  fndifnfp  7181  f1ounsn  7280  f12dfv  7281  f13dfv  7282  resf1extb  7946  infpssrlem4  10387  sqrt2irr  16422  sdrgunit  21058  prmidlval  21623  dsmmval  22045  dsmmbas2  22048  frlmbas  22066  dfconn2  23742  alexsublem  24368  uc1pval  26463  mon1pval  26465  dchrsum2  27600  flt4ALT  27997  fltoprm  28000  noetainflem4  28102  isinag  29362  elcgrabasi  29380  uhgrwkspthlem2  30345  usgr2wlkneq  30347  usgr2trlspth  30352  lfgrn1cycl  30399  uspgrn2crct  30402  2pthdlem1  30524  3pthdlem1  30770  numclwwlk2lem1  30982  eigorth  32445  eighmorth  32571  mxidlval  34032  ressply1mon1p  34146  extdgfialglem1  34370  wlimeq12  36673  limsucncmpi  37325  mh-inf3f1  37421  poimirlem25  38656  poimirlem26  38657  pridlval  39060  maxidlval  39066  lshpset  40128  lduallkr3  40312  isatl  40449  cdlemk42  42091  prjspnnorm  43754  dffltz  43763  stoweidlem43  47146  nnfoctbdjlem  47558  fuconuniqex  50879  fuconuniqex2  50880