Theorem neeq1d 2352

Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.)

Hypothesis

Ref	Expression
neeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
neeq1d	⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Proof of Theorem neeq1d

Step	Hyp	Ref	Expression
1		neeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		neeq1 2347	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1342   ≠ wne 2334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-5 1434  ax-gen 1436  ax-4 1497  ax-17 1513  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-cleq 2157  df-ne 2335

This theorem is referenced by:  neeq12d  2354  eqnetrd  2358  prnzg  3694  hashprg  10710  algcvg  11959  algcvga  11962  eucalgcvga  11969  rpdvds  12010  phibndlem  12125  dfphi2  12129  pcaddlem  12247  ennnfoneleminc  12281  ennnfonelemex  12284  ennnfonelemhom  12285  ennnfonelemnn0  12292  ennnfonelemr  12293  ennnfonelemim  12294  ctinfomlemom  12297  dceqnconst  13772  dcapnconst  13773  nconstwlpolem  13777