Theorem neeq2 2417

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 2241	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
2	1	notbid 673	. 2 ⊢ (𝐴 = 𝐵 → (¬ 𝐶 = 𝐴 ↔ ¬ 𝐶 = 𝐵))
3		df-ne 2404	. 2 ⊢ (𝐶 ≠ 𝐴 ↔ ¬ 𝐶 = 𝐴)
4		df-ne 2404	. 2 ⊢ (𝐶 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐵)
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))

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

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 619  ax-in2 620  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-ne 2404

This theorem is referenced by:  neeq2i  2419  neeq2d  2422  disji2  4085  fodjuomnilemdc  7386  netap  7516  2oneel  7518  2omotaplemap  7519  2omotaplemst  7520  exmidapne  7522  xrlttri3  10076  hashdmprop2dom  11154  fun2dmnop0  11160  isnzr2  14262  umgrvad2edg  16135  eupth2lem3lem4fi  16397  3dom  16691  qdiff  16764  neapmkv  16784  neap0mkv  16785  ltlenmkv  16786