MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.24 Structured version   Unicode version

Theorem pm2.24 112
Description: Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 136. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
pm2.24  |-  ( ph  ->  ( -.  ph  ->  ps ) )

Proof of Theorem pm2.24
StepHypRef Expression
1 pm2.21 111 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
21com12 32 1  |-  ( ph  ->  ( -.  ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm4.81  367  orc  386  pm2.82  860  dedlema  962  cases2  980  eqneqall  2631  suppimacnv  6933  ressuppss  6942  ressuppssdif  6944  infssuni  7868  axpowndlem1  9023  ltlen  9736  znnn0nn  11048  elfzonlteqm1  11989  injresinjlem  12024  ssnn0fi  12197  hasheqf1oi  12534  swrdnd2  12780  swrdccat3blem  12842  repswswrd  12878  mdegle0  23013  nb3graprlem1  25165  nbcusgra  25177  wlkdvspthlem  25323  clwwlkprop  25484  hashnbgravdg  25627  4cyclusnfrgra  25733  broutsideof2  30882  meran1  31064  bj-andnotim  31164  contrd  32247  pell1qrgaplem  35639  pm2.43cbi  36733  zeo2ALTV  38512  elnelall  38692  ztprmneprm  39402
  Copyright terms: Public domain W3C validator