Theorem neeq2 2389

Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)

Assertion

Ref	Expression
neeq2	⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))

Proof of Theorem neeq2

Step	Hyp	Ref	Expression
1		eqeq2 2214	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
2	1	notbid 668	. 2 ⊢ (𝐴 = 𝐵 → (¬ 𝐶 = 𝐴 ↔ ¬ 𝐶 = 𝐵))
3		df-ne 2376	. 2 ⊢ (𝐶 ≠ 𝐴 ↔ ¬ 𝐶 = 𝐴)
4		df-ne 2376	. 2 ⊢ (𝐶 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐵)
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105   = wceq 1372   ≠ wne 2375

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-ne 2376

This theorem is referenced by:  neeq2i  2391  neeq2d  2394  disji2  4036  fodjuomnilemdc  7245  netap  7365  2oneel  7367  2omotaplemap  7368  2omotaplemst  7369  exmidapne  7371  xrlttri3  9918  hashdmprop2dom  10987  fun2dmnop0  10990  isnzr2  13888  neapmkv  15940  neap0mkv  15941  ltlenmkv  15942