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 728  meredith 920  r19.27av 1730  vtoclegft 1831  tfindsg 3125  xrub 5978  caun0 7828  bcthlem2 7882  efilcp 8795  efilcp2 8800

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

Copyright terms: Public domain