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  730  pm2.82  820  pm4.81dc  916  dedlema  978  ifp2  989  alexim  1694  eqneqall  2413  elnelall  2510  sotritric  4427  ltxrlt  8287  zltnle  9569  elfzonlteqm1  10501  qltnle  10549  hashfzp1  11134  swrdccat3blem  11369  dfgcd2  12648  oddprmdvds  12990  2lgsoddprm  15915  bj-fast  16442  nnnotnotr  16689