Theorem neeq1 2416

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

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

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 2213

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

This theorem is referenced by:  neeq1i  2418  neeq1d  2421  nelrdva  3014  disji2  4085  0inp0  4262  frecabcl  6608  fiintim  7166  eldju2ndl  7314  updjudhf  7321  netap  7516  2oneel  7518  2omotaplemap  7519  2omotaplemst  7520  exmidapne  7522  xnn0nemnf  9519  uzn0  9815  xrnemnf  10055  xrnepnf  10056  ngtmnft  10095  xsubge0  10159  xposdif  10160  xleaddadd  10165  fztpval  10361  hashdmprop2dom  11152  fun2dmnop0  11158  pcpre1  12926  pcqmul  12937  pcqcl  12940  xpsfrnel  13488  isnzr2  14260  fiinopn  14795  umgrvad2edg  16132  isclwwlk  16315  eupth2lem2dc  16380  eupth2lem3lem6fi  16392  eupth2lem3lem4fi  16394  3dom  16688  pw1ndom3lem  16689  qdiff  16761  neapmkv  16781  neap0mkv  16782  ltlenmkv  16783