Theorem neeq1d 2421

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ≠ wne 2403

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 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-ne 2404

This theorem is referenced by:  neeq12d  2423  eqnetrd  2427  prnzg  3801  suppval1  6417  elsuppfng  6420  elsuppfn  6421  suppsnopdc  6428  ressuppss  6432  pw2f1odclem  7063  hashprg  11116  algcvg  12681  algcvga  12684  eucalgcvga  12691  rpdvds  12732  phibndlem  12849  dfphi2  12853  pcaddlem  12973  ennnfoneleminc  13093  ennnfonelemex  13096  ennnfonelemhom  13097  ennnfonelemnn0  13104  ennnfonelemr  13105  ennnfonelemim  13106  ctinfomlemom  13109  setscomd  13184  pellexlem3  15773  lgsne0  15837  umgr2cwwkdifex  16346  dceqnconst  16773  dcapnconst  16774  nconstwlpolem  16778