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

Theorem pm2.24 593
Description: Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
pm2.24  |-  ( ph  ->  ( -.  ph  ->  ps ) )

Proof of Theorem pm2.24
StepHypRef Expression
1 pm2.21 589 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
21com12 30 1  |-  ( ph  ->  ( -.  ph  ->  ps ) )
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 587
This theorem is referenced by:  pm2.24d  594  pm2.53  694  pm2.82  784  pm4.81dc  876  dedlema  936  alexim  1607  eqneqall  2293  elnelall  2390  sotritric  4214  ltxrlt  7794  zltnle  9051  elfzonlteqm1  9927  qltnle  9963  hashfzp1  10510  dfgcd2  11598  bj-fast  12775
  Copyright terms: Public domain W3C validator