Theorem pm2.24 626

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 622	. 2 |- ( -. ph -> ( ph -> ps ) )
2	1	com12 30	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-in2 620

This theorem is referenced by:  pm2.24d  627  pm2.53  729  pm2.82  819  pm4.81dc  915  dedlema  977  ifp2  988  alexim  1693  eqneqall  2412  elnelall  2509  sotritric  4421  ltxrlt  8244  zltnle  9524  elfzonlteqm1  10454  qltnle  10502  hashfzp1  11087  swrdccat3blem  11319  dfgcd2  12584  oddprmdvds  12926  2lgsoddprm  15841  bj-fast  16337  nnnotnotr  16585