Theorem pm2.24 630

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 626	. 2 |- ( -. ph -> ( ph -> ps ) )
2	1	com12 30	1 |- ( ph -> ( -. ph -> ps ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 624

This theorem is used by:  pm2.24d  631  pm2.53  734  pm2.82  824  pm4.81dc  920  dedlema  982  ifp2  993  alexim  1698  eqneqall  2430  elnelall  2527  sotritric  4469  ltxrlt  8391  zltnle  9690  elfzonlteqm1  10628  qltnle  10678  hashfzp1  11265  swrdccat3blem  11511  dfgcd2  12791  oddprmdvds  13133  2lgsoddprm  16232  bj-fast  16769  nnnotnotr  17016