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

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

Proof of Theorem pm2.24
StepHypRef Expression
1 pm2.21 112 . 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  372  orc  391  pm2.82  868  dedlema  971  cases2  989  eqneqall  2645  suppimacnv  6951  ressuppss  6960  ressuppssdif  6962  infssuni  7890  axpowndlem1  9047  ltlen  9760  znnn0nn  11075  elfzonlteqm1  12019  injresinjlem  12055  ssnn0fi  12228  hasheqf1oi  12565  swrdnd2  12825  swrdccat3blem  12887  repswswrd  12923  mdegle0  23074  nb3graprlem1  25227  nbcusgra  25239  wlkdvspthlem  25385  clwwlkprop  25546  hashnbgravdg  25689  4cyclusnfrgra  25795  broutsideof2  30937  meran1  31119  bj-andnotim  31216  contrd  32377  pell1qrgaplem  35763  pm2.43cbi  36918  zeo2ALTV  38837  elnelall  39019  nb3grprlem1  39503  ztprmneprm  40400
  Copyright terms: Public domain W3C validator