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  8219  ltlen  8922  mdegle0  19463  broutsideof2  24745  meran1  24850  isunscov  25074  lineval6a  26089  isconcl5a  26101  isconcl5ab  26102  pdiveql  26168  pell1qrgaplem  26958  pellfundex  26971  monotoddzzfi  27027  jm2.23  27089  nbusgra  28143  nbcusgra  28159  pm2.43cbi  28280
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator