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  1667  eqneqall  2385  elnelall  2482  sotritric  4370  ltxrlt  8137  zltnle  9417  elfzonlteqm1  10337  qltnle  10384  hashfzp1  10967  dfgcd2  12277  oddprmdvds  12619  2lgsoddprm  15532  bj-fast  15610  nnnotnotr  15859