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  8187  ltlen  8890  mdegle0  19426  broutsideof2  24121  meran1  24226  isunscov  24441  lineval6a  25457  isconcl5a  25469  isconcl5ab  25470  pdiveql  25536  pell1qrgaplem  26326  pellfundex  26339  monotoddzzfi  26395  jm2.23  26457  pm2.43cbi  27416
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator