MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.24 Unicode version

Theorem pm2.24 103
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 102 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
21com12 29 1  |-  ( ph  ->  ( -.  ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  pm4.81  357  orc  376  pm2.82  828  dedlema  925  axpowndlem1  8152  ltlen  8855  mdegle0  19390  broutsideof2  24085  meran1  24190  isunscov  24405  lineval6a  25421  isconcl5a  25433  isconcl5ab  25434  pdiveql  25500  pell1qrgaplem  26290  pellfundex  26303  monotoddzzfi  26359  jm2.23  26421  pm2.43cbi  27296
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator