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  6565  fiintim  7123  eldju2ndl  7271  updjudhf  7278  netap  7473  2oneel  7475  2omotaplemap  7476  2omotaplemst  7477  exmidapne  7479  xnn0nemnf  9476  uzn0  9772  xrnemnf  10012  xrnepnf  10013  ngtmnft  10052  xsubge0  10116  xposdif  10117  xleaddadd  10122  fztpval  10318  hashdmprop2dom  11109  fun2dmnop0  11115  pcpre1  12883  pcqmul  12894  pcqcl  12897  xpsfrnel  13445  isnzr2  14217  fiinopn  14747  umgrvad2edg  16081  isclwwlk  16264  eupth2lem2dc  16329  eupth2lem3lem6fi  16341  eupth2lem3lem4fi  16343  3dom  16638  pw1ndom3lem  16639  qdiff  16704  neapmkv  16724  neap0mkv  16725  ltlenmkv  16726