Theorem neeq2d 3021

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

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

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 2156  ax-ext 2738

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

This theorem is used by:  neeq2  3024  neeqtrd  3030  prneprprc  4831  fndifnfp  7181  f1ounsn  7281  f12dfv  7282  f13dfv  7283  resf1extb  7940  infpssrlem4  10308  sqrt2irr  16330  sdrgunit  20936  prmidlval  21499  dsmmval  21921  dsmmbas2  21924  frlmbas  21942  dfconn2  23613  alexsublem  24238  uc1pval  26334  mon1pval  26336  dchrsum2  27469  noetainflem4  27941  isinag  29192  uhgrwkspthlem2  30140  usgr2wlkneq  30142  usgr2trlspth  30147  lfgrn1cycl  30191  uspgrn2crct  30194  2pthdlem1  30316  3pthdlem1  30552  numclwwlk2lem1  30764  eigorth  32227  eighmorth  32353  mxidlval  33775  ressply1mon1p  33889  extdgfialglem1  34113  wlimeq12  36330  limsucncmpi  36997  poimirlem25  38337  poimirlem26  38338  pridlval  38725  maxidlval  38731  lshpset  39793  lduallkr3  39977  isatl  40114  cdlemk42  41756  prjspner1  43399  dffltz  43407  stoweidlem43  46798  nnfoctbdjlem  47210