Theorem pm2.24 610

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 606	. 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 604

This theorem is referenced by:  pm2.24d  611  pm2.53  711  pm2.82  801  pm4.81dc  893  dedlema  953  alexim  1624  eqneqall  2318  elnelall  2415  sotritric  4246  ltxrlt  7830  zltnle  9100  elfzonlteqm1  9987  qltnle  10023  hashfzp1  10570  dfgcd2  11702  bj-fast  12952