Theorem pm2.27 62

Description: This theorem, called "Assertion," can be thought of as closed form of modus ponens. Theorem *2.27 of [WhiteheadRussell] p. 104.

Assertion

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

Proof of Theorem pm2.27

Step	Hyp	Ref	Expression
1		id 59	. 2 |- ((ph -> ps) -> (ph -> ps))
2	1	com12 11	1 |- (ph -> ((ph -> ps) -> ps))

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.43 63  pm3.2im 122  mth8 123  a1bi 197  pm3.35 359  pm2.75 574  biimt 731  meredith 924  ax10o 1139  r19.27av 1754  vtoclegft 1856  tfindsg 3162  xrub 6080  caun0 7945  bcthlem2 8000  dmdbr5 10235  efilcp 10572  efilcpOLD 10573  efilcp2 10581  efilcp2OLD 10582

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

Copyright terms: Public domain