Theorem neeq1d 2363

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ≠ wne 2345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-5 1445  ax-gen 1447  ax-4 1508  ax-17 1524  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-cleq 2168  df-ne 2346

This theorem is referenced by:  neeq12d  2365  eqnetrd  2369  prnzg  3713  hashprg  10756  algcvg  12015  algcvga  12018  eucalgcvga  12025  rpdvds  12066  phibndlem  12183  dfphi2  12187  pcaddlem  12305  ennnfoneleminc  12379  ennnfonelemex  12382  ennnfonelemhom  12383  ennnfonelemnn0  12390  ennnfonelemr  12391  ennnfonelemim  12392  ctinfomlemom  12395  lgsne0  14019  dceqnconst  14377  dcapnconst  14378  nconstwlpolem  14382