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  a2andOLD  812  pm2.26  883  cases2  971  cases2OLD  972  19.35  1674  axc112  1923  axc11n-16  2254  axc11-o  2267  issref  5370  tfinds  6679  tfindsg  6680  smogt  7040  findcard2  7762  findcard3  7765  fisupg  7770  xpfi  7793  dffi2  7885  cantnfle  8093  cantnfleOLD  8123  ac5num  8420  pwsdompw  8587  cfsmolem  8653  axcc4  8822  axdc3lem2  8834  fpwwe2lem8  9018  pwfseqlem3  9041  tskord  9161  grudomon  9198  grur1a  9200  xrub  11512  pcmptcl  14287  restntr  19556  cmpsublem  19772  cmpsub  19773  bwthOLD  19784  txlm  20022  ptcmplem3  20427  c1lip1  22271  wilthlem3  23216  dmdbr5  27099  wzel  29355  waj-ax  29854  lukshef-ax2  29855  finixpnum  30013  mbfresfi  30036  filbcmb  30206  orfa  30454  axc5c4c711toc7  31265  axc5c4c711to11  31266  snlindsntor  32802  ax6e2nd  33059  elex22VD  33367  exbiriVD  33382  ssralv2VD  33394  truniALTVD  33406  trintALTVD  33408  onfrALTVD  33419  hbimpgVD  33432  ax6e2eqVD  33435  ax6e2ndVD  33436  bj-axd2d  33923