Theorem neeq1d 2395

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   ≠ wne 2377

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-ne 2378

This theorem is referenced by:  neeq12d  2397  eqnetrd  2401  prnzg  3760  pw2f1odclem  6943  hashprg  10966  algcvg  12420  algcvga  12423  eucalgcvga  12430  rpdvds  12471  phibndlem  12588  dfphi2  12592  pcaddlem  12712  ennnfoneleminc  12832  ennnfonelemex  12835  ennnfonelemhom  12836  ennnfonelemnn0  12843  ennnfonelemr  12844  ennnfonelemim  12845  ctinfomlemom  12848  setscomd  12923  lgsne0  15565  dceqnconst  16114  dcapnconst  16115  nconstwlpolem  16119