Theorem neeq2d 2991

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ≠ wne 2931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-ne 2932

This theorem is referenced by:  neeq2  2994  neeqtrd  3000  prneprprc  4843  fndifnfp  7179  f1ounsn  7275  f12dfv  7276  f13dfv  7277  resf1extb  7939  infpssrlem4  10329  sqrt2irr  16268  sdrgunit  20770  dsmmval  21721  dsmmbas2  21724  frlmbas  21742  dfconn2  23392  alexsublem  24017  uc1pval  26134  mon1pval  26136  dchrsum2  27267  noetainflem4  27740  isinag  28801  uhgrwkspthlem2  29721  usgr2wlkneq  29723  usgr2trlspth  29728  lfgrn1cycl  29772  uspgrn2crct  29775  2pthdlem1  29897  3pthdlem1  30130  numclwwlk2lem1  30342  eigorth  31804  eighmorth  31930  prmidlval  33406  mxidlval  33430  ressply1mon1p  33534  wlimeq12  35761  limsucncmpi  36387  poimirlem25  37593  poimirlem26  37594  pridlval  37981  maxidlval  37987  lshpset  38920  lduallkr3  39104  isatl  39241  cdlemk42  40884  prjspner1  42581  dffltz  42589  stoweidlem43  46003  nnfoctbdjlem  46415