Theorem pm2.24 112

Description: Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 136. (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 111	. 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  367  orc  386  pm2.82  860  dedlema  962  cases2  980  eqneqall  2631  suppimacnv  6933  ressuppss  6942  ressuppssdif  6944  infssuni  7868  axpowndlem1  9023  ltlen  9736  znnn0nn  11048  elfzonlteqm1  11989  injresinjlem  12024  ssnn0fi  12197  hasheqf1oi  12534  swrdnd2  12780  swrdccat3blem  12842  repswswrd  12878  mdegle0  23013  nb3graprlem1  25165  nbcusgra  25177  wlkdvspthlem  25323  clwwlkprop  25484  hashnbgravdg  25627  4cyclusnfrgra  25733  broutsideof2  30882  meran1  31064  bj-andnotim  31164  contrd  32247  pell1qrgaplem  35639  pm2.43cbi  36733  zeo2ALTV  38512  elnelall  38692  ztprmneprm  39402