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  8221  ltlen  8924  mdegle0  19465  broutsideof2  24747  meran1  24852  isunscov  25085  lineval6a  26100  isconcl5a  26112  isconcl5ab  26113  pdiveql  26179  pell1qrgaplem  26969  pellfundex  26982  monotoddzzfi  27038  jm2.23  27100  nbusgra  28154  nbcusgra  28170  pm2.43cbi  28336
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator