Theorem neeq1 2360

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

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

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 614  ax-in2 615  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-ne 2348

This theorem is referenced by:  neeq1i  2362  neeq1d  2365  nelrdva  2945  disji2  3997  0inp0  4167  frecabcl  6400  fiintim  6928  eldju2ndl  7071  updjudhf  7078  netap  7253  2oneel  7255  2omotaplemap  7256  2omotaplemst  7257  exmidapne  7259  xnn0nemnf  9250  uzn0  9543  xrnemnf  9777  xrnepnf  9778  ngtmnft  9817  xsubge0  9881  xposdif  9882  xleaddadd  9887  fztpval  10083  pcpre1  12292  pcqmul  12303  pcqcl  12306  xpsfrnel  12763  fiinopn  13507  neapmkv  14818  neap0mkv  14819  ltlenmkv  14820