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  3743  pw2f1odclem  6892  hashprg  10882  algcvg  12189  algcvga  12192  eucalgcvga  12199  rpdvds  12240  phibndlem  12357  dfphi2  12361  pcaddlem  12480  ennnfoneleminc  12571  ennnfonelemex  12574  ennnfonelemhom  12575  ennnfonelemnn0  12582  ennnfonelemr  12583  ennnfonelemim  12584  ctinfomlemom  12587  setscomd  12662  lgsne0  15195  dceqnconst  15620  dcapnconst  15621  nconstwlpolem  15625