Theorem pm2.27 35

Description: This theorem, called "Assertion," can be thought of as closed form of modus ponens ax-mp 5. Theorem *2.27 of [WhiteheadRussell] p. 104. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem pm2.27

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

Syntax hints:   -> wi 4

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

This theorem is referenced by:  pm2.43  47  com23  72  pm3.2im  137  mth8  138  biimt  325  pm3.35  570  pm2.26  853  dvelimv  1939  ax10lem6  1943  ax10o  1952  ax10-16  2190  ax10o-o  2203  eqfnfv  5393  dff3  5421  weds  5939  ncssfin  6152  nclenn  6250