Theorem neeq1 2433

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 105   = wceq 1402   ≠ wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-ne 2421

This theorem is used by:  neeq1i  2435  neeq1d  2438  nelrdva  3033  disji2  4122  0inp0  4303  frecabcl  6670  fiintim  7238  eldju2ndl  7412  updjudhf  7419  netap  7620  2oneel  7622  2omotaplemap  7623  2omotaplemst  7624  exmidapne  7626  xnn0nemnf  9645  uzn0  9947  xrnemnf  10189  xrnepnf  10190  ngtmnft  10229  xsubge0  10293  xposdif  10294  xleaddadd  10299  fztpval  10500  hashdmprop2dom  11310  fun2dmnop0  11316  pcpre1  13091  pcqmul  13102  pcqcl  13105  xpsfrnel  13714  isnzr2  14540  fiinopn  15154  umgrvad2edg  16550  isclwwlk  16733  eupth2lem2dc  16798  eupth2lem3lem6fi  16810  eupth2lem3lem4fi  16812  3dom  17116  pw1ndom3lem  17117  qdiff  17196  neapmkv  17216  neap0mkv  17217  ltlenmkv  17218