Theorem neeq1d 2324

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 2319	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1331   ≠ wne 2306

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 603  ax-in2 604  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-ne 2307

This theorem is referenced by:  neeq12d  2326  eqnetrd  2330  prnzg  3642  hashprg  10547  algcvg  11718  algcvga  11721  eucalgcvga  11728  rpdvds  11769  phibndlem  11881  dfphi2  11885  ennnfoneleminc  11913  ennnfonelemex  11916  ennnfonelemhom  11917  ennnfonelemnn0  11924  ennnfonelemr  11925  ennnfonelemim  11926  ctinfomlemom  11929