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  10917  algcvg  12241  algcvga  12244  eucalgcvga  12251  rpdvds  12292  phibndlem  12409  dfphi2  12413  pcaddlem  12533  ennnfoneleminc  12653  ennnfonelemex  12656  ennnfonelemhom  12657  ennnfonelemnn0  12664  ennnfonelemr  12665  ennnfonelemim  12666  ctinfomlemom  12669  setscomd  12744  lgsne0  15363  dceqnconst  15791  dcapnconst  15792  nconstwlpolem  15796