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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  neeq2  2996  neeqtrd  3002  prneprprc  4805  fndifnfp  7124  f1ounsn  7220  f12dfv  7221  f13dfv  7222  resf1extb  7878  infpssrlem4  10219  sqrt2irr  16207  sdrgunit  20764  dsmmval  21724  dsmmbas2  21727  frlmbas  21745  dfconn2  23394  alexsublem  24019  uc1pval  26115  mon1pval  26117  dchrsum2  27245  noetainflem4  27718  isinag  28920  uhgrwkspthlem2  29837  usgr2wlkneq  29839  usgr2trlspth  29844  lfgrn1cycl  29888  uspgrn2crct  29891  2pthdlem1  30013  3pthdlem1  30249  numclwwlk2lem1  30461  eigorth  31924  eighmorth  32050  prmidlval  33512  mxidlval  33536  ressply1mon1p  33643  extdgfialglem1  33852  wlimeq12  36015  limsucncmpi  36643  poimirlem25  37980  poimirlem26  37981  pridlval  38368  maxidlval  38374  lshpset  39438  lduallkr3  39622  isatl  39759  cdlemk42  41401  prjspner1  43073  dffltz  43081  stoweidlem43  46489  nnfoctbdjlem  46901