Theorem neeq1d 2365

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ≠ wne 2347

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 614  ax-in2 615  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-ne 2348

This theorem is referenced by:  neeq12d  2367  eqnetrd  2371  prnzg  3718  hashprg  10790  algcvg  12050  algcvga  12053  eucalgcvga  12060  rpdvds  12101  phibndlem  12218  dfphi2  12222  pcaddlem  12340  ennnfoneleminc  12414  ennnfonelemex  12417  ennnfonelemhom  12418  ennnfonelemnn0  12425  ennnfonelemr  12426  ennnfonelemim  12427  ctinfomlemom  12430  setscomd  12505  lgsne0  14524  dceqnconst  14893  dcapnconst  14894  nconstwlpolem  14898