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

Theorem pm2.24 622
Description: Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
pm2.24 (𝜑 → (¬ 𝜑𝜓))

Proof of Theorem pm2.24
StepHypRef Expression
1 pm2.21 618 . 2 𝜑 → (𝜑𝜓))
21com12 30 1 (𝜑 → (¬ 𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 616
This theorem is referenced by:  pm2.24d  623  pm2.53  723  pm2.82  813  pm4.81dc  909  dedlema  971  alexim  1656  eqneqall  2370  elnelall  2467  sotritric  4342  ltxrlt  8054  zltnle  9330  elfzonlteqm1  10242  qltnle  10278  hashfzp1  10839  dfgcd2  12050  oddprmdvds  12389  bj-fast  14971  nnnotnotr  15220
  Copyright terms: Public domain W3C validator