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  848  dedlema  945  cases2  963  eqneqall  2710  prnebg  4059  suppimacnv  6706  ressuppss  6713  ressuppssdif  6715  infssuni  7607  axpowndlem1  8766  ltlen  9481  injresinjlem  11643  hasheqf1oi  12127  swrdnd  12331  swrdvalodm2  12338  swrdvalodm  12339  swrdccat3blem  12391  repswswrd  12427  mdegle0  21553  usgra2edg  23306  nb3graprlem1  23364  nbcusgra  23376  wlkdvspthlem  23511  hashnbgravdg  23586  broutsideof2  28158  meran1  28262  contrd  28905  pell1qrgaplem  29219  elnelall  30121  elfzonlteqm1  30230  clwwlkprop  30438  4cyclusnfrgra  30616  frgrawopreglem4  30645  ztprmneprm  30744  ssnn0fi  30751  pm2.43cbi  31228  bj-iftru  32094  bj-andnotim  32119