Theorem neeq1 2425

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-ne 2413

This theorem is referenced by:  neeq1i  2427  neeq1d  2430  nelrdva  3024  disji2  4101  0inp0  4279  frecabcl  6630  fiintim  7191  eldju2ndl  7363  updjudhf  7370  netap  7568  2oneel  7570  2omotaplemap  7571  2omotaplemst  7572  exmidapne  7574  xnn0nemnf  9574  uzn0  9870  xrnemnf  10110  xrnepnf  10111  ngtmnft  10150  xsubge0  10214  xposdif  10215  xleaddadd  10220  fztpval  10417  hashdmprop2dom  11216  fun2dmnop0  11222  pcpre1  12990  pcqmul  13001  pcqcl  13004  xpsfrnel  13557  isnzr2  14329  fiinopn  14869  umgrvad2edg  16206  isclwwlk  16389  eupth2lem2dc  16454  eupth2lem3lem6fi  16466  eupth2lem3lem4fi  16468  3dom  16762  pw1ndom3lem  16763  qdiff  16833  neapmkv  16854  neap0mkv  16855  ltlenmkv  16856