Theorem neeq2d 2988

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ≠ wne 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929

This theorem is referenced by:  neeq2  2991  neeqtrd  2997  prneprprc  4813  fndifnfp  7110  f1ounsn  7206  f12dfv  7207  f13dfv  7208  resf1extb  7864  infpssrlem4  10197  sqrt2irr  16158  sdrgunit  20712  dsmmval  21672  dsmmbas2  21675  frlmbas  21693  dfconn2  23335  alexsublem  23960  uc1pval  26073  mon1pval  26075  dchrsum2  27207  noetainflem4  27680  isinag  28817  uhgrwkspthlem2  29733  usgr2wlkneq  29735  usgr2trlspth  29740  lfgrn1cycl  29784  uspgrn2crct  29787  2pthdlem1  29909  3pthdlem1  30142  numclwwlk2lem1  30354  eigorth  31816  eighmorth  31942  prmidlval  33400  mxidlval  33424  ressply1mon1p  33529  extdgfialglem1  33703  wlimeq12  35859  limsucncmpi  36485  poimirlem25  37691  poimirlem26  37692  pridlval  38079  maxidlval  38085  lshpset  39023  lduallkr3  39207  isatl  39344  cdlemk42  40986  prjspner1  42665  dffltz  42673  stoweidlem43  46087  nnfoctbdjlem  46499