Theorem pm2.24 109

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

Step	Hyp	Ref	Expression
1		pm2.21 108	. 2 |- ( -. ph -> ( ph -> ps ) )
2	1	com12 31	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  366  orc  385  pm2.82  852  dedlema  954  cases2  971  cases2OLD  972  eqneqall  2650  suppimacnv  6914  ressuppss  6921  ressuppssdif  6923  infssuni  7813  axpowndlem1  8975  ltlen  9689  elfzonlteqm1  11873  injresinjlem  11907  ssnn0fi  12076  hasheqf1oi  12406  swrdnd  12639  swrdvalodm2  12646  swrdvalodm  12647  swrdccat3blem  12702  repswswrd  12738  mdegle0  22455  nb3graprlem1  24429  nbcusgra  24441  wlkdvspthlem  24587  clwwlkprop  24748  hashnbgravdg  24891  4cyclusnfrgra  24997  broutsideof2  29748  meran1  29852  contrd  30473  pell1qrgaplem  30785  znnn0nn  31443  elnelall  32247  ztprmneprm  32804  pm2.43cbi  33156  bj-iftru  34035  bj-andnotim  34060