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  8392  zltnle  9695  elfzonlteqm1  10639  qltnle  10689  hashfzp1  11281  swrdccat3blem  11527  dfgcd2  12810  oddprmdvds  13156  2lgsoddprm  16398  bj-fast  16935  nnnotnotr  17182