Theorem pm2.24 95

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

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm4.81 180  oridmOLD 263  orc 291  pm5.63 373  pm2.8 636  pm2.82 638  dedlema 837  dedlemaOLD 838  prlem1OLD 849  dn1OLD 856  axpowndlem1 6101  ltlen 6692  ioojoin 7585  dif1card 10177  eucalglt 13753  meran1 14235  isunscov 14386

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

Copyright terms: Public domain