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  850  dedlema  952  cases2  970  cases2OLD  971  eqneqall  2674  prnebg  4208  suppimacnv  6912  ressuppss  6919  ressuppssdif  6921  infssuni  7811  axpowndlem1  8972  ltlen  9686  elfzonlteqm1  11859  injresinjlem  11893  ssnn0fi  12062  hasheqf1oi  12392  swrdnd  12620  swrdvalodm2  12627  swrdvalodm  12628  swrdccat3blem  12683  repswswrd  12719  mdegle0  22240  usgra2edg  24086  nb3graprlem1  24155  nbcusgra  24167  wlkdvspthlem  24313  clwwlkprop  24474  hashnbgravdg  24617  4cyclusnfrgra  24723  frgrawopreglem4  24752  broutsideof2  29377  meran1  29481  contrd  30128  pell1qrgaplem  30441  znnn0nn  31094  elnelall  31788  ztprmneprm  32032  pm2.43cbi  32385  bj-iftru  33251  bj-andnotim  33276