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

Theorem pm2.53 712
Description: Theorem *2.53 of [WhiteheadRussell] p. 107. This holds intuitionistically, although its converse does not (see pm2.54dc 877). (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 611 . 2 (𝜑 → (¬ 𝜑𝜓))
2 ax-1 6 . 2 (𝜓 → (¬ 𝜑𝜓))
31, 2jaoi 706 1 ((𝜑𝜓) → (¬ 𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wo 698
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 605  ax-io 699
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ori  713  ord  714  orel1  715  pm2.63  790  notnotrdc  829  dfordc  878  pm5.6r  913  xorbin  1366  19.33b2  1609  r19.30dc  2604  onsucelsucexmid  4489  oprabidlem  5852  omnimkv  7099  xnn0nnn0pnf  9166  absle  10989
  Copyright terms: Public domain W3C validator