Theorem pm2.27 39

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, 15-Jul-1993.)

Assertion

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

Proof of Theorem pm2.27

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ( ph -> ps ) -> ( ph -> ps ) )
2	1	com12 31	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  51  com23  78  pm3.2im  145  mth8  146  biimt  335  pm3.35  587  pm2.26  878  cases2  963  19.35  1655  axc112  1872  axc11n-16  2246  axc11-o  2259  issref  5311  tfinds  6572  tfindsg  6573  smogt  6930  findcard2  7655  findcard3  7658  fisupg  7663  xpfi  7686  dffi2  7776  cantnfle  7982  cantnfleOLD  8012  ac5num  8309  pwsdompw  8476  cfsmolem  8542  axcc4  8711  axdc3lem2  8723  fpwwe2lem8  8907  pwfseqlem3  8930  tskord  9050  grudomon  9087  grur1a  9089  xrub  11377  pcmptcl  14057  restntr  18904  cmpsublem  19120  cmpsub  19121  bwthOLD  19132  txlm  19339  ptcmplem3  19744  c1lip1  21587  wilthlem3  22526  dmdbr5  25849  wzel  27897  waj-ax  28396  lukshef-ax2  28397  finixpnum  28554  mbfresfi  28578  filbcmb  28774  orfa  29022  axc5c4c711toc7  29798  axc5c4c711to11  29799  a2and  30856  snlindsntor  31114  ax6e2nd  31569  elex22VD  31877  exbiriVD  31892  ssralv2VD  31904  truniALTVD  31916  trintALTVD  31918  onfrALTVD  31929  hbimpgVD  31942  ax6e2eqVD  31945  ax6e2ndVD  31946  bj-axd2d  32430