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

Step	Hyp	Ref	Expression
1		pm2.21 112	. 2 |- ( -. ph -> ( ph -> ps ) )
2	1	com12 32	1 |- ( ph -> ( -. ph -> ps ) )

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