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  2424  elnelall  2521  sotritric  4450  ltxrlt  8355  zltnle  9640  elfzonlteqm1  10577  qltnle  10627  hashfzp1  11214  swrdccat3blem  11456  dfgcd2  12735  oddprmdvds  13077  2lgsoddprm  16112  bj-fast  16639  nnnotnotr  16886