Theorem neeq1 2415

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

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

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  neeq1i  2417  neeq1d  2420  nelrdva  3013  disji2  4080  0inp0  4256  frecabcl  6564  fiintim  7122  eldju2ndl  7270  updjudhf  7277  netap  7472  2oneel  7474  2omotaplemap  7475  2omotaplemst  7476  exmidapne  7478  xnn0nemnf  9475  uzn0  9771  xrnemnf  10011  xrnepnf  10012  ngtmnft  10051  xsubge0  10115  xposdif  10116  xleaddadd  10121  fztpval  10317  hashdmprop2dom  11107  fun2dmnop0  11110  pcpre1  12864  pcqmul  12875  pcqcl  12878  xpsfrnel  13426  isnzr2  14197  fiinopn  14727  umgrvad2edg  16061  isclwwlk  16244  eupth2lem2dc  16309  3dom  16587  pw1ndom3lem  16588  neapmkv  16672  neap0mkv  16673  ltlenmkv  16674