Theorem neeq1 2370

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

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

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 615  ax-in2 616  ax-5 1457  ax-gen 1459  ax-4 1520  ax-17 1536  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-ne 2358

This theorem is referenced by:  neeq1i  2372  neeq1d  2375  nelrdva  2956  disji2  4008  0inp0  4178  frecabcl  6414  fiintim  6942  eldju2ndl  7085  updjudhf  7092  netap  7267  2oneel  7269  2omotaplemap  7270  2omotaplemst  7271  exmidapne  7273  xnn0nemnf  9264  uzn0  9557  xrnemnf  9791  xrnepnf  9792  ngtmnft  9831  xsubge0  9895  xposdif  9896  xleaddadd  9901  fztpval  10097  pcpre1  12306  pcqmul  12317  pcqcl  12320  xpsfrnel  12782  fiinopn  13857  neapmkv  15170  neap0mkv  15171  ltlenmkv  15172