Theorem neeq2d 2842

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  neeq2  2845  neeqtrd  2851  fndifnfp  6347  f12dfv  6429  f13dfv  6430  infpssrlem4  9011  sqrt2irr  14817  dsmmval  19897  dsmmbas2  19900  frlmbas  19918  dfcon2  21032  alexsublem  21658  uc1pval  23703  mon1pval  23705  dchrsum2  24793  isinag  25529  usgrcyclnl1  26168  numclwwlkovq  26626  eigorth  28081  eighmorth  28207  wlimeq12  31009  nofulllem5  31105  limsucncmpi  31614  poimirlem25  32604  poimirlem26  32605  pridlval  33002  maxidlval  33008  lshpset  33283  lduallkr3  33467  isatl  33604  cdlemk42  35247  stoweidlem43  38936  nnfoctbdjlem  39348  uhgr1wlkspthlem2  40960  usgr2wlkneq  40962  usgr2trlspth  40967  lfgrn1cycl  41008  uspgrn2crct  41011  2pthdlem1  41137  3pthdlem1  41331  av-numclwwlk2lem1  41532