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  3747  pw2f1odclem  6904  hashprg  10919  algcvg  12243  algcvga  12246  eucalgcvga  12253  rpdvds  12294  phibndlem  12411  dfphi2  12415  pcaddlem  12535  ennnfoneleminc  12655  ennnfonelemex  12658  ennnfonelemhom  12659  ennnfonelemnn0  12666  ennnfonelemr  12667  ennnfonelemim  12668  ctinfomlemom  12671  setscomd  12746  lgsne0  15387  dceqnconst  15817  dcapnconst  15818  nconstwlpolem  15822