Theorem neeq1d 2385

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-ne 2368

This theorem is referenced by:  neeq12d  2387  eqnetrd  2391  prnzg  3746  pw2f1odclem  6895  hashprg  10900  algcvg  12216  algcvga  12219  eucalgcvga  12226  rpdvds  12267  phibndlem  12384  dfphi2  12388  pcaddlem  12508  ennnfoneleminc  12628  ennnfonelemex  12631  ennnfonelemhom  12632  ennnfonelemnn0  12639  ennnfonelemr  12640  ennnfonelemim  12641  ctinfomlemom  12644  setscomd  12719  lgsne0  15279  dceqnconst  15704  dcapnconst  15705  nconstwlpolem  15709