Theorem neeq2d 2993

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  neeq2  2996  neeqtrd  3002  prneprprc  4819  fndifnfp  7132  f1ounsn  7228  f12dfv  7229  f13dfv  7230  resf1extb  7886  infpssrlem4  10228  sqrt2irr  16186  sdrgunit  20741  dsmmval  21701  dsmmbas2  21704  frlmbas  21722  dfconn2  23375  alexsublem  24000  uc1pval  26113  mon1pval  26115  dchrsum2  27247  noetainflem4  27720  isinag  28922  uhgrwkspthlem2  29839  usgr2wlkneq  29841  usgr2trlspth  29846  lfgrn1cycl  29890  uspgrn2crct  29893  2pthdlem1  30015  3pthdlem1  30251  numclwwlk2lem1  30463  eigorth  31925  eighmorth  32051  prmidlval  33529  mxidlval  33553  ressply1mon1p  33660  extdgfialglem1  33869  wlimeq12  36030  limsucncmpi  36658  poimirlem25  37890  poimirlem26  37891  pridlval  38278  maxidlval  38284  lshpset  39348  lduallkr3  39532  isatl  39669  cdlemk42  41311  prjspner1  42978  dffltz  42986  stoweidlem43  46395  nnfoctbdjlem  46807