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

Theorem pm2.53 723
Description: Theorem *2.53 of [WhiteheadRussell] p. 107. This holds intuitionistically, although its converse does not (see pm2.54dc 892). (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 622 . 2 (𝜑 → (¬ 𝜑𝜓))
2 ax-1 6 . 2 (𝜓 → (¬ 𝜑𝜓))
31, 2jaoi 717 1 ((𝜑𝜓) → (¬ 𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wo 709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 616  ax-io 710
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  ori  724  ord  725  orel1  726  pm2.63  801  notnotrdc  844  dfordc  893  pm5.6r  928  xorbin  1395  19.33b2  1640  r19.30dc  2637  onsucelsucexmid  4550  oprabidlem  5931  omnimkv  7189  xnn0nnn0pnf  9287  absle  11139
  Copyright terms: Public domain W3C validator