Theorem neeq2d 2854

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483   ≠ wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  neeq2  2857  neeqtrd  2863  fndifnfp  6442  f12dfv  6529  f13dfv  6530  infpssrlem4  9128  sqrt2irr  14979  dsmmval  20078  dsmmbas2  20081  frlmbas  20099  dfconn2  21222  alexsublem  21848  uc1pval  23899  mon1pval  23901  dchrsum2  24993  isinag  25729  uhgrwkspthlem2  26650  usgr2wlkneq  26652  usgr2trlspth  26657  lfgrn1cycl  26697  uspgrn2crct  26700  2pthdlem1  26826  3pthdlem1  27024  numclwwlk2lem1  27235  eigorth  28697  eighmorth  28823  wlimeq12  31765  limsucncmpi  32444  poimirlem25  33434  poimirlem26  33435  pridlval  33832  maxidlval  33838  lshpset  34265  lduallkr3  34449  isatl  34586  cdlemk42  36229  stoweidlem43  40260  nnfoctbdjlem  40672