Theorem neeq2d 3001

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ≠ wne 2940

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-ne 2941

This theorem is referenced by:  neeq2  3004  neeqtrd  3010  prneprprc  4861  fndifnfp  7176  f12dfv  7273  f13dfv  7274  infpssrlem4  10303  sqrt2irr  16196  sdrgunit  20555  dsmmval  21508  dsmmbas2  21511  frlmbas  21529  dfconn2  23143  alexsublem  23768  uc1pval  25881  mon1pval  25883  dchrsum2  26995  noetainflem4  27467  isinag  28344  uhgrwkspthlem2  29266  usgr2wlkneq  29268  usgr2trlspth  29273  lfgrn1cycl  29314  uspgrn2crct  29317  2pthdlem1  29439  3pthdlem1  29672  numclwwlk2lem1  29884  eigorth  31346  eighmorth  31472  prmidlval  32817  mxidlval  32839  ressply1mon1p  32919  wlimeq12  35083  limsucncmpi  35633  poimirlem25  36816  poimirlem26  36817  pridlval  37204  maxidlval  37210  lshpset  38151  lduallkr3  38335  isatl  38472  cdlemk42  40115  prjspner1  41670  dffltz  41678  stoweidlem43  45058  nnfoctbdjlem  45470