Theorem neeq1d 2432

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

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

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 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-ne 2415

This theorem is referenced by:  neeq12d  2434  eqnetrd  2438  prnzg  3822  suppval1  6452  elsuppfng  6455  elsuppfn  6456  suppsnopdc  6463  ressuppss  6467  pw2f1odclem  7100  hashprg  11198  algcvg  12770  algcvga  12773  eucalgcvga  12780  rpdvds  12821  phibndlem  12938  dfphi2  12942  pcaddlem  13062  ennnfoneleminc  13246  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemnn0  13257  ennnfonelemr  13258  ennnfonelemim  13259  ctinfomlemom  13262  setscomd  13337  rrgsupp  14497  pellexlem3  15959  lgsne0  16023  umgr2cwwkdifex  16532  dceqnconst  16958  dcapnconst  16959  nconstwlpolem  16963