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  2944  disji2  3996  0inp0  4166  frecabcl  6399  fiintim  6927  eldju2ndl  7070  updjudhf  7077  netap  7252  2oneel  7254  2omotaplemap  7255  2omotaplemst  7256  exmidapne  7258  xnn0nemnf  9249  uzn0  9542  xrnemnf  9776  xrnepnf  9777  ngtmnft  9816  xsubge0  9880  xposdif  9881  xleaddadd  9886  fztpval  10082  pcpre1  12291  pcqmul  12302  pcqcl  12305  xpsfrnel  12762  fiinopn  13474  neapmkv  14785  neap0mkv  14786  ltlenmkv  14787