New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  neeq1 GIF version

Theorem neeq1 2524
 Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
Assertion
Ref Expression
neeq1 (A = B → (ACBC))

Proof of Theorem neeq1
StepHypRef Expression
1 eqeq1 2359 . . 3 (A = B → (A = CB = C))
21notbid 285 . 2 (A = B → (¬ A = C ↔ ¬ B = C))
3 df-ne 2518 . 2 (AC ↔ ¬ A = C)
4 df-ne 2518 . 2 (BC ↔ ¬ B = C)
52, 3, 43bitr4g 279 1 (A = B → (ACBC))
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator