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  8099  ltlen  8802  mdegle0  19295  broutsideof2  23919  meran1  24024  isunscov  24239  lineval6a  25255  isconcl5a  25267  isconcl5ab  25268  pdiveql  25334  pell1qrgaplem  26124  pellfundex  26137  monotoddzzfi  26193  jm2.23  26255  pm2.43cbi  26973
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator