Theorem neeq2d 2994

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1542   ≠ wne 2934

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 1975  ax-7 2020  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2730  df-ne 2935

This theorem is referenced by:  neeq2  2997  neeqtrd  3003  prneprprc  4746  fndifnfp  6948  f12dfv  7041  f13dfv  7042  infpssrlem4  9806  sqrt2irr  15694  dsmmval  20550  dsmmbas2  20553  frlmbas  20571  dfconn2  22170  alexsublem  22795  uc1pval  24892  mon1pval  24894  dchrsum2  26004  isinag  26784  uhgrwkspthlem2  27695  usgr2wlkneq  27697  usgr2trlspth  27702  lfgrn1cycl  27743  uspgrn2crct  27746  2pthdlem1  27868  3pthdlem1  28101  numclwwlk2lem1  28313  eigorth  29773  eighmorth  29899  prmidlval  31184  mxidlval  31205  wlimeq12  33424  noetainflem4  33584  limsucncmpi  34272  poimirlem25  35425  poimirlem26  35426  pridlval  35814  maxidlval  35820  lshpset  36615  lduallkr3  36799  isatl  36936  cdlemk42  38578  prjspner1  40040  dffltz  40043  stoweidlem43  43126  nnfoctbdjlem  43535