Theorem neeq2d 2985

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  neeq2  2988  neeqtrd  2994  prneprprc  4825  fndifnfp  7150  f1ounsn  7247  f12dfv  7248  f13dfv  7249  resf1extb  7910  infpssrlem4  10259  sqrt2irr  16217  sdrgunit  20705  dsmmval  21643  dsmmbas2  21646  frlmbas  21664  dfconn2  23306  alexsublem  23931  uc1pval  26045  mon1pval  26047  dchrsum2  27179  noetainflem4  27652  isinag  28765  uhgrwkspthlem2  29684  usgr2wlkneq  29686  usgr2trlspth  29691  lfgrn1cycl  29735  uspgrn2crct  29738  2pthdlem1  29860  3pthdlem1  30093  numclwwlk2lem1  30305  eigorth  31767  eighmorth  31893  prmidlval  33408  mxidlval  33432  ressply1mon1p  33537  wlimeq12  35807  limsucncmpi  36433  poimirlem25  37639  poimirlem26  37640  pridlval  38027  maxidlval  38033  lshpset  38971  lduallkr3  39155  isatl  39292  cdlemk42  40935  prjspner1  42614  dffltz  42622  stoweidlem43  46041  nnfoctbdjlem  46453