Theorem pm2.27 40

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 30	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  53  com23  78  biimt  240  pm3.35  344  pm3.2im  626  jcn  640  pm2.65  648  annimim  675  condcOLD  839  pm2.26dc  892  ax10o  1693  issref  4921  acexmidlem2  5771  findcard2  6783  findcard2s  6784  xpfi  6818  txlm  12448  bj-inf2vnlem1  13168  bj-findis  13177