Theorem neeq2i 2847

Description: Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Hypothesis

Ref	Expression
neeq1i.1	⊢ 𝐴 = 𝐵

Assertion

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

Proof of Theorem neeq2i

Step	Hyp	Ref	Expression
1		neeq1i.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	eqeq2i 2622	. 2 ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)
3	2	necon3bii 2834	1 ⊢ (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)

Syntax hints:   ↔ wb 195   = wceq 1475   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  neeqtri  2854  suppvalbr  7186  disjdsct  28863  divnumden2  28951  nosgnn0  31055  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352