Theorem neeq1d 2378

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ≠ wne 2360

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 615  ax-in2 616  ax-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-ne 2361

This theorem is referenced by:  neeq12d  2380  eqnetrd  2384  prnzg  3731  pw2f1odclem  6863  hashprg  10823  algcvg  12083  algcvga  12086  eucalgcvga  12093  rpdvds  12134  phibndlem  12251  dfphi2  12255  pcaddlem  12374  ennnfoneleminc  12465  ennnfonelemex  12468  ennnfonelemhom  12469  ennnfonelemnn0  12476  ennnfonelemr  12477  ennnfonelemim  12478  ctinfomlemom  12481  setscomd  12556  lgsne0  14917  dceqnconst  15287  dcapnconst  15288  nconstwlpolem  15292