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  9694  elfzonlteqm1  10638  qltnle  10688  hashfzp1  11279  swrdccat3blem  11525  dfgcd2  12807  oddprmdvds  13153  2lgsoddprm  16330  bj-fast  16867  nnnotnotr  17114