Theorem pm2.24 127

Description: Theorem *2.24 of [WhiteheadRussell] p. 104.

Assertion

Ref	Expression
pm2.24	|- (ph -> (-. ph -> ps))

Proof of Theorem pm2.24

Step	Hyp	Ref	Expression
1		pm2.21 124	. 2 |- (-. ph -> (ph -> ps))
2	1	com12 26	1 |- (ph -> (-. ph -> ps))

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm4.81 308  orc 376  pm2.8OLD 913  pm2.82 915  pm5.63OLD 1041  dedlema 1082  pm2.43cbi 1575  dif1cardOLD 6144  axpowndlem1 6467  ltlen 6881  ioojoin 7931  eucalglt 9348  meran1 14935  isunscov 15096

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

Copyright terms: Public domain