Theorem neeq1d 2438

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402   ≠ wne 2420

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 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is referenced by:  neeq12d  2440  eqnetrd  2444  prnzg  3836  suppval1  6473  elsuppfng  6476  elsuppfn  6477  suppsnopdc  6484  ressuppss  6488  pw2f1odclem  7128  hashprg  11232  algcvg  12809  algcvga  12812  eucalgcvga  12819  rpdvds  12860  phibndlem  12977  dfphi2  12981  pcaddlem  13101  ennnfoneleminc  13285  ennnfonelemex  13288  ennnfonelemhom  13289  ennnfonelemnn0  13296  ennnfonelemr  13297  ennnfonelemim  13298  ctinfomlemom  13301  setscomd  13376  rrgsupp  14557  pellexlem3  16076  lgsne0  16140  umgr2cwwkdifex  16649  dceqnconst  17084  dcapnconst  17085  nconstwlpolem  17089