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  241  pm3.35  347  pm3.2im  637  jcn  651  pm2.65  659  annimim  686  condcOLD  854  pm2.26dc  907  ax10o  1715  issref  5012  acexmidlem2  5872  findcard2  6889  findcard2s  6890  xpfi  6929  exmidontriim  7224  pcmptcl  12340  txlm  13782  bj-inf2vnlem1  14725  bj-findis  14734