Theorem neeq1 2525

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 2519	. 2 ⊢ (A ≠ C ↔ ¬ A = C)
4		df-ne 2519	. 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 2517

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 2519

This theorem is referenced by:  neeq1i  2527  neeq1d  2530  psseq1  3357  opkltfing  4450  ltfintri  4467  tfin11  4494  0ceven  4506  evennn  4507  oddnn  4508  evennnul  4509  oddnnul  4510  sucevenodd  4511  sucoddeven  4512  dfevenfin2  4513  dfoddfin2  4514  evenoddnnnul  4515  evenodddisjlem1  4516  eventfin  4518  oddtfin  4519  nulnnn  4557  xp11  5057  tz6.12i  5349  frd  5923  elqsn0  5994  enprmapc  6084  ce2  6193  nchoicelem14  6303