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  4305  frecabcl  6674  fiintim  7242  eldju2ndl  7418  updjudhf  7425  netap  7626  2oneel  7628  2omotaplemap  7629  2omotaplemst  7630  exmidapne  7632  xnn0nemnf  9652  uzn0  9954  xrnemnf  10196  xrnepnf  10197  ngtmnft  10236  xsubge0  10300  xposdif  10301  xleaddadd  10306  fztpval  10507  hashdmprop2dom  11318  fun2dmnop0  11324  pcpre1  13100  pcqmul  13111  pcqcl  13114  xpsfrnel  13724  isnzr2  14600  fiinopn  15230  umgrvad2edg  16657  isclwwlk  16840  eupth2lem2dc  16905  eupth2lem3lem6fi  16917  eupth2lem3lem4fi  16919  3dom  17223  pw1ndom3lem  17224  qdiff  17305  neapmkv  17325  neap0mkv  17326  ltlenmkv  17327