Theorem neeq2d 2995

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ne 2936

This theorem is referenced by:  neeq2  2998  neeqtrd  3004  prneprprc  4799  fndifnfp  7127  f1ounsn  7223  f12dfv  7224  f13dfv  7225  resf1extb  7881  infpssrlem4  10226  sqrt2irr  16214  sdrgunit  20775  dsmmval  21716  dsmmbas2  21719  frlmbas  21737  dfconn2  23409  alexsublem  24034  uc1pval  26130  mon1pval  26132  dchrsum2  27256  noetainflem4  27729  isinag  28931  uhgrwkspthlem2  29847  usgr2wlkneq  29849  usgr2trlspth  29854  lfgrn1cycl  29898  uspgrn2crct  29901  2pthdlem1  30023  3pthdlem1  30259  numclwwlk2lem1  30471  eigorth  31934  eighmorth  32060  prmidlval  33527  mxidlval  33551  ressply1mon1p  33658  extdgfialglem1  33883  wlimeq12  36052  limsucncmpi  36680  poimirlem25  38019  poimirlem26  38020  pridlval  38407  maxidlval  38413  lshpset  39477  lduallkr3  39661  isatl  39798  cdlemk42  41440  prjspner1  43083  dffltz  43091  stoweidlem43  46493  nnfoctbdjlem  46905