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  6483  elsuppfng  6486  elsuppfn  6487  suppsnopdc  6494  ressuppss  6498  pw2f1odclem  7139  hashprg  11272  algcvg  12852  algcvga  12855  eucalgcvga  12862  rpdvds  12903  phibndlem  13024  dfphi2  13028  pcaddlem  13148  ennnfoneleminc  13361  ennnfonelemex  13364  ennnfonelemhom  13365  ennnfonelemnn0  13372  ennnfonelemr  13373  ennnfonelemim  13374  ctinfomlemom  13377  setscomd  13452  rrgsupp  14684  pellexlem3  16243  lgsne0  16374  umgr2cwwkdifex  16883  dceqnconst  17329  dcapnconst  17330  nconstwlpolem  17334