Theorem neeq1 2524

Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)

Assertion

Ref	Expression
neeq1	⊢ (A = B → (A ≠ C ↔ B ≠ C))

Proof of Theorem neeq1

Step	Hyp	Ref	Expression
1		eqeq1 2359	. . 3 ⊢ (A = B → (A = C ↔ B = C))
2	1	notbid 285	. 2 ⊢ (A = B → (¬ A = C ↔ ¬ B = C))
3		df-ne 2518	. 2 ⊢ (A ≠ C ↔ ¬ A = C)
4		df-ne 2518	. 2 ⊢ (B ≠ C ↔ ¬ B = C)
5	2, 3, 4	3bitr4g 279	1 ⊢ (A = B → (A ≠ C ↔ B ≠ C))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   = wceq 1642   ≠ wne 2516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346  df-ne 2518

This theorem is referenced by:  neeq1i  2526  neeq1d  2529  psseq1  3356  opkltfing  4449  ltfintri  4466  tfin11  4493  0ceven  4505  evennn  4506  oddnn  4507  evennnul  4508  oddnnul  4509  sucevenodd  4510  sucoddeven  4511  dfevenfin2  4512  dfoddfin2  4513  evenoddnnnul  4514  evenodddisjlem1  4515  eventfin  4517  oddtfin  4518  nulnnn  4556  xp11  5056  tz6.12i  5348  frd  5922  elqsn0  5993  enprmapc  6083  ce2  6192  nchoicelem14  6302