Theorem neeq1d 2438

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ≠ wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is used by:  neeq12d  2440  eqnetrd  2444  prnzg  3838  suppval1  6479  elsuppfng  6482  elsuppfn  6483  suppsnopdc  6490  ressuppss  6494  pw2f1odclem  7134  hashprg  11264  algcvg  12844  algcvga  12847  eucalgcvga  12854  rpdvds  12895  phibndlem  13016  dfphi2  13020  pcaddlem  13140  ennnfoneleminc  13353  ennnfonelemex  13356  ennnfonelemhom  13357  ennnfonelemnn0  13364  ennnfonelemr  13365  ennnfonelemim  13366  ctinfomlemom  13369  setscomd  13444  rrgsupp  14625  pellexlem3  16153  lgsne0  16279  umgr2cwwkdifex  16788  dceqnconst  17232  dcapnconst  17233  nconstwlpolem  17237