Theorem neeq2i 2436

Description: Inference for inequality. (Contributed by NM, 29-Apr-2005.)

Hypothesis

Ref	Expression
neeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
neeq2i	⊢ (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)

Proof of Theorem neeq2i

Step	Hyp	Ref	Expression
1		neeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		neeq2 2434	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)

This proof depends on syntax axioms:   ↔ 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:  neeq12i  2437  neeqtri  2447  exmidsbthrlem  17067