Theorem pm2.24 121

Description: Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 146. (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 120	. 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  381  orc  400  pm2.82  897  cases2  993  dedlema  1002  eqneqall  2805  elnelall  2910  ordnbtwn  5816  suppimacnv  7306  ressuppss  7314  ressuppssdif  7316  infssuni  8257  axpowndlem1  9419  ltlen  10138  znnn0nn  11489  elfzonlteqm1  12543  injresinjlem  12588  addmodlteq  12745  ssnn0fi  12784  hasheqf1oi  13140  hasheqf1oiOLD  13141  hashfzp1  13218  swrdnd2  13433  swrdccat3blem  13495  repswswrd  13531  dvdsaddre2b  15029  dfgcd2  15263  prm23ge5  15520  oddprmdvds  15607  mdegle0  23837  2lgsoddprm  25141  nb3grprlem1  26282  4cyclusnfrgr  27156  broutsideof2  32229  meran1  32410  bj-andnotim  32573  contrd  33899  pell1qrgaplem  37437  clsk1indlem3  38341  pm2.43cbi  38724  zeo2ALTV  41582  ztprmneprm  42125