Theorem neeq2d 2989

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ≠ wne 2929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ne 2930

This theorem is referenced by:  neeq2  2992  neeqtrd  2998  prneprprc  4812  fndifnfp  7116  f1ounsn  7212  f12dfv  7213  f13dfv  7214  resf1extb  7870  infpssrlem4  10204  sqrt2irr  16160  sdrgunit  20713  dsmmval  21673  dsmmbas2  21676  frlmbas  21694  dfconn2  23335  alexsublem  23960  uc1pval  26073  mon1pval  26075  dchrsum2  27207  noetainflem4  27680  isinag  28817  uhgrwkspthlem2  29734  usgr2wlkneq  29736  usgr2trlspth  29741  lfgrn1cycl  29785  uspgrn2crct  29788  2pthdlem1  29910  3pthdlem1  30146  numclwwlk2lem1  30358  eigorth  31820  eighmorth  31946  prmidlval  33409  mxidlval  33433  ressply1mon1p  33538  extdgfialglem1  33726  wlimeq12  35882  limsucncmpi  36510  poimirlem25  37706  poimirlem26  37707  pridlval  38094  maxidlval  38100  lshpset  39098  lduallkr3  39282  isatl  39419  cdlemk42  41061  prjspner1  42745  dffltz  42753  stoweidlem43  46166  nnfoctbdjlem  46578