Theorem neeq1d 2358

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348   ≠ wne 2340

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 609  ax-in2 610  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-ne 2341

This theorem is referenced by:  neeq12d  2360  eqnetrd  2364  prnzg  3707  hashprg  10743  algcvg  12002  algcvga  12005  eucalgcvga  12012  rpdvds  12053  phibndlem  12170  dfphi2  12174  pcaddlem  12292  ennnfoneleminc  12366  ennnfonelemex  12369  ennnfonelemhom  12370  ennnfonelemnn0  12377  ennnfonelemr  12378  ennnfonelemim  12379  ctinfomlemom  12382  lgsne0  13733  dceqnconst  14091  dcapnconst  14092  nconstwlpolem  14096