Theorem neeq1d 2398

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1375   ≠ wne 2380

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 617  ax-in2 618  ax-5 1473  ax-gen 1475  ax-4 1536  ax-17 1552  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-cleq 2202  df-ne 2381

This theorem is referenced by:  neeq12d  2400  eqnetrd  2404  prnzg  3771  pw2f1odclem  6963  hashprg  10997  algcvg  12536  algcvga  12539  eucalgcvga  12546  rpdvds  12587  phibndlem  12704  dfphi2  12708  pcaddlem  12828  ennnfoneleminc  12948  ennnfonelemex  12951  ennnfonelemhom  12952  ennnfonelemnn0  12959  ennnfonelemr  12960  ennnfonelemim  12961  ctinfomlemom  12964  setscomd  13039  lgsne0  15682  dceqnconst  16339  dcapnconst  16340  nconstwlpolem  16344