Theorem neeq1d 2420

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   ≠ wne 2402

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 619  ax-in2 620  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-ne 2403

This theorem is referenced by:  neeq12d  2422  eqnetrd  2426  prnzg  3797  pw2f1odclem  7020  hashprg  11073  algcvg  12625  algcvga  12628  eucalgcvga  12635  rpdvds  12676  phibndlem  12793  dfphi2  12797  pcaddlem  12917  ennnfoneleminc  13037  ennnfonelemex  13040  ennnfonelemhom  13041  ennnfonelemnn0  13048  ennnfonelemr  13049  ennnfonelemim  13050  ctinfomlemom  13053  setscomd  13128  lgsne0  15773  umgr2cwwkdifex  16282  dceqnconst  16690  dcapnconst  16691  nconstwlpolem  16695