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 6068  caun0 7930  bcthlem2 7985  dmdbr5 10220  efilcp 10530  efilcp2 10536

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

Copyright terms: Public domain