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  8215  ltlen  8918  mdegle0  19459  broutsideof2  24155  meran1  24260  isunscov  24484  lineval6a  25500  isconcl5a  25512  isconcl5ab  25513  pdiveql  25579  pell1qrgaplem  26369  pellfundex  26382  monotoddzzfi  26438  jm2.23  26500  pm2.43cbi  27563
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator