ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.53 GIF version

Theorem pm2.53 717
Description: Theorem *2.53 of [WhiteheadRussell] p. 107. This holds intuitionistically, although its converse does not (see pm2.54dc 886). (Contributed by NM, 3-Jan-2005.) (Revised by NM, 31-Jan-2015.)
Assertion
Ref Expression
pm2.53 ((𝜑𝜓) → (¬ 𝜑𝜓))

Proof of Theorem pm2.53
StepHypRef Expression
1 pm2.24 616 . 2 (𝜑 → (¬ 𝜑𝜓))
2 ax-1 6 . 2 (𝜓 → (¬ 𝜑𝜓))
31, 2jaoi 711 1 ((𝜑𝜓) → (¬ 𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wo 703
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 610  ax-io 704
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ori  718  ord  719  orel1  720  pm2.63  795  notnotrdc  838  dfordc  887  pm5.6r  922  xorbin  1379  19.33b2  1622  r19.30dc  2617  onsucelsucexmid  4514  oprabidlem  5884  omnimkv  7132  xnn0nnn0pnf  9211  absle  11053
  Copyright terms: Public domain W3C validator