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 572  biimt 729  meredith 921  ax10o 1135  r19.27av 1746  vtoclegft 1847  tfindsg 3152  xrub 6027  caun0 7880  bcthlem2 7934  efilcp 10445  efilcp2 10450

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

Copyright terms: Public domain