Theorem neeq1 2427

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

Assertion

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

Proof of Theorem neeq1

Step	Hyp	Ref	Expression
1		eqeq1 2241	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2	1	notbid 673	. 2 ⊢ (𝐴 = 𝐵 → (¬ 𝐴 = 𝐶 ↔ ¬ 𝐵 = 𝐶))
3		df-ne 2415	. 2 ⊢ (𝐴 ≠ 𝐶 ↔ ¬ 𝐴 = 𝐶)
4		df-ne 2415	. 2 ⊢ (𝐵 ≠ 𝐶 ↔ ¬ 𝐵 = 𝐶)
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

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

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 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-ne 2415

This theorem is referenced by:  neeq1i  2429  neeq1d  2432  nelrdva  3027  disji2  4106  0inp0  4284  frecabcl  6643  fiintim  7204  eldju2ndl  7376  updjudhf  7383  netap  7584  2oneel  7586  2omotaplemap  7587  2omotaplemst  7588  exmidapne  7590  xnn0nemnf  9591  uzn0  9888  xrnemnf  10129  xrnepnf  10130  ngtmnft  10169  xsubge0  10233  xposdif  10234  xleaddadd  10239  fztpval  10439  hashdmprop2dom  11241  fun2dmnop0  11247  pcpre1  13015  pcqmul  13026  pcqcl  13029  xpsfrnel  13608  isnzr2  14429  fiinopn  14995  umgrvad2edg  16332  isclwwlk  16515  eupth2lem2dc  16580  eupth2lem3lem6fi  16592  eupth2lem3lem4fi  16594  3dom  16888  pw1ndom3lem  16889  qdiff  16959  neapmkv  16980  neap0mkv  16981  ltlenmkv  16982