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  4471  ltxrlt  8397  zltnle  9699  elfzonlteqm1  10644  qltnle  10694  hashfzp1  11286  swrdccat3blem  11532  dfgcd2  12815  oddprmdvds  13161  2lgsoddprm  16454  bj-fast  16991  nnnotnotr  17238