Theorem neeq1d 2382

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ≠ wne 2364

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 615  ax-in2 616  ax-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-ne 2365

This theorem is referenced by:  neeq12d  2384  eqnetrd  2388  prnzg  3742  pw2f1odclem  6890  hashprg  10879  algcvg  12186  algcvga  12189  eucalgcvga  12196  rpdvds  12237  phibndlem  12354  dfphi2  12358  pcaddlem  12477  ennnfoneleminc  12568  ennnfonelemex  12571  ennnfonelemhom  12572  ennnfonelemnn0  12579  ennnfonelemr  12580  ennnfonelemim  12581  ctinfomlemom  12584  setscomd  12659  lgsne0  15154  dceqnconst  15550  dcapnconst  15551  nconstwlpolem  15555