Theorem neeq2 2416

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

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

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  neeq2i  2418  neeq2d  2421  disji2  4080  fodjuomnilemdc  7342  netap  7472  2oneel  7474  2omotaplemap  7475  2omotaplemst  7476  exmidapne  7478  xrlttri3  10031  hashdmprop2dom  11107  fun2dmnop0  11110  isnzr2  14197  umgrvad2edg  16061  3dom  16587  neapmkv  16672  neap0mkv  16673  ltlenmkv  16674