Theorem neeq1d 2430

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-ne 2413

This theorem is referenced by:  neeq12d  2432  eqnetrd  2436  prnzg  3816  suppval1  6438  elsuppfng  6441  elsuppfn  6442  suppsnopdc  6449  ressuppss  6453  pw2f1odclem  7086  hashprg  11171  algcvg  12741  algcvga  12744  eucalgcvga  12751  rpdvds  12792  phibndlem  12909  dfphi2  12913  pcaddlem  13033  ennnfoneleminc  13154  ennnfonelemex  13157  ennnfonelemhom  13158  ennnfonelemnn0  13165  ennnfonelemr  13166  ennnfonelemim  13167  ctinfomlemom  13170  setscomd  13245  rrgsupp  14403  pellexlem3  15839  lgsne0  15903  umgr2cwwkdifex  16412  dceqnconst  16837  dcapnconst  16838  nconstwlpolem  16842