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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

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

This theorem is referenced by:  neeq2  2996  neeqtrd  3002  prneprprc  4842  fndifnfp  7173  f1ounsn  7270  f12dfv  7271  f13dfv  7272  resf1extb  7935  infpssrlem4  10325  sqrt2irr  16272  sdrgunit  20761  dsmmval  21699  dsmmbas2  21702  frlmbas  21720  dfconn2  23362  alexsublem  23987  uc1pval  26102  mon1pval  26104  dchrsum2  27236  noetainflem4  27709  isinag  28822  uhgrwkspthlem2  29741  usgr2wlkneq  29743  usgr2trlspth  29748  lfgrn1cycl  29792  uspgrn2crct  29795  2pthdlem1  29917  3pthdlem1  30150  numclwwlk2lem1  30362  eigorth  31824  eighmorth  31950  prmidlval  33457  mxidlval  33481  ressply1mon1p  33586  wlimeq12  35842  limsucncmpi  36468  poimirlem25  37674  poimirlem26  37675  pridlval  38062  maxidlval  38068  lshpset  39001  lduallkr3  39185  isatl  39322  cdlemk42  40965  prjspner1  42624  dffltz  42632  stoweidlem43  46052  nnfoctbdjlem  46464