Theorem neeq1 2390

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

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

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 615  ax-in2 616  ax-5 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-ne 2378

This theorem is referenced by:  neeq1i  2392  neeq1d  2395  nelrdva  2984  disji2  4043  0inp0  4218  frecabcl  6498  fiintim  7043  eldju2ndl  7189  updjudhf  7196  netap  7386  2oneel  7388  2omotaplemap  7389  2omotaplemst  7390  exmidapne  7392  xnn0nemnf  9389  uzn0  9684  xrnemnf  9919  xrnepnf  9920  ngtmnft  9959  xsubge0  10023  xposdif  10024  xleaddadd  10029  fztpval  10225  hashdmprop2dom  11011  fun2dmnop0  11014  pcpre1  12690  pcqmul  12701  pcqcl  12704  xpsfrnel  13251  isnzr2  14021  fiinopn  14551  neapmkv  16148  neap0mkv  16149  ltlenmkv  16150