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  4818  fndifnfp  7124  f1ounsn  7220  f12dfv  7221  f13dfv  7222  resf1extb  7878  infpssrlem4  10220  sqrt2irr  16178  sdrgunit  20733  dsmmval  21693  dsmmbas2  21696  frlmbas  21714  dfconn2  23367  alexsublem  23992  uc1pval  26105  mon1pval  26107  dchrsum2  27239  noetainflem4  27712  isinag  28893  uhgrwkspthlem2  29810  usgr2wlkneq  29812  usgr2trlspth  29817  lfgrn1cycl  29861  uspgrn2crct  29864  2pthdlem1  29986  3pthdlem1  30222  numclwwlk2lem1  30434  eigorth  31896  eighmorth  32022  prmidlval  33499  mxidlval  33523  ressply1mon1p  33630  extdgfialglem1  33830  wlimeq12  35992  limsucncmpi  36620  poimirlem25  37817  poimirlem26  37818  pridlval  38205  maxidlval  38211  lshpset  39275  lduallkr3  39459  isatl  39596  cdlemk42  41238  prjspner1  42905  dffltz  42913  stoweidlem43  46323  nnfoctbdjlem  46735