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  11201  algcvg  12774  algcvga  12777  eucalgcvga  12784  rpdvds  12825  phibndlem  12942  dfphi2  12946  pcaddlem  13066  ennnfoneleminc  13250  ennnfonelemex  13253  ennnfonelemhom  13254  ennnfonelemnn0  13261  ennnfonelemr  13262  ennnfonelemim  13263  ctinfomlemom  13266  setscomd  13341  rrgsupp  14516  pellexlem3  15977  lgsne0  16041  umgr2cwwkdifex  16550  dceqnconst  16985  dcapnconst  16986  nconstwlpolem  16990