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

Theorem pm2.24 101
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 100 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
21com12 27 1  |-  ( ph  ->  ( -.  ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm4.81  355  orc  374  pm2.82  825  dedlema  920  axpowndlem1  8235  ltlen  8938  mdegle0  19479  broutsideof2  24817  meran1  24922  isunscov  25177  lineval6a  26192  isconcl5a  26204  isconcl5ab  26205  pdiveql  26271  pell1qrgaplem  27061  pellfundex  27074  monotoddzzfi  27130  jm2.23  27192  injresinjlem  28214  nbusgra  28277  nb3graprlem1  28287  nbcusgra  28298  wlkdvspthlem  28365  pm2.43cbi  28579
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator