Theorem neeq2d 3019

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ne 2960

This theorem is used by:  neeq2  3022  neeqtrd  3028  prneprprc  4819  fndifnfp  7204  f1ounsn  7303  f12dfv  7304  f13dfv  7305  resf1extb  7970  infpssrlem4  10411  sqrt2irr  16446  sdrgunit  21083  prmidlval  21648  dsmmval  22070  dsmmbas2  22073  frlmbas  22091  dfconn2  23767  alexsublem  24393  uc1pval  26488  mon1pval  26490  dchrsum2  27625  flt4ALT  28022  fltoprm  28025  noetainflem4  28127  isinag  29387  elcgrabasi  29405  uhgrwkspthlem2  30370  usgr2wlkneq  30372  usgr2trlspth  30377  lfgrn1cycl  30424  uspgrn2crct  30427  2pthdlem1  30549  3pthdlem1  30795  numclwwlk2lem1  31007  eigorth  32470  eighmorth  32596  mxidlval  34056  ressply1mon1p  34170  extdgfialglem1  34394  wlimeq12  36759  limsucncmpi  37411  mh-inf3f1  37507  poimirlem25  38755  poimirlem26  38756  pridlval  39159  maxidlval  39165  lshpset  40227  lduallkr3  40411  isatl  40548  cdlemk42  42190  prjspnnorm  43854  dffltz  43863  stoweidlem43  47258  nnfoctbdjlem  47670  fuconuniqex  50991  fuconuniqex2  50992