Theorem pm2.24 622

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 618	. 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 616

This theorem is referenced by:  pm2.24d  623  pm2.53  723  pm2.82  813  pm4.81dc  909  dedlema  971  alexim  1656  eqneqall  2370  elnelall  2467  sotritric  4342  ltxrlt  8052  zltnle  9328  elfzonlteqm1  10239  qltnle  10275  hashfzp1  10835  dfgcd2  12046  oddprmdvds  12385  bj-fast  14946  nnnotnotr  15195