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  333  pm3.35  585  a2andOLD  810  pm2.26  881  cases2  969  19.35  1692  axc112  1942  axc11n-16  2270  axc11-o  2283  issref  5368  tfinds  6667  tfindsg  6668  smogt  7030  findcard2  7752  findcard3  7755  fisupg  7760  xpfi  7783  dffi2  7875  cantnfle  8081  cantnfleOLD  8111  ac5num  8408  pwsdompw  8575  cfsmolem  8641  axcc4  8810  axdc3lem2  8822  fpwwe2lem8  9004  pwfseqlem3  9027  tskord  9147  grudomon  9184  grur1a  9186  xrub  11506  relexprelg  12953  pcmptcl  14494  restntr  19850  cmpsublem  20066  cmpsub  20067  txlm  20315  ptcmplem3  20720  c1lip1  22564  wilthlem3  23542  dmdbr5  27425  wzel  29620  waj-ax  30107  lukshef-ax2  30108  finixpnum  30278  mbfresfi  30301  filbcmb  30471  orfa  30719  axc5c4c711toc7  31552  axc5c4c711to11  31553  snlindsntor  33326  ax6e2nd  33725  elex22VD  34039  exbiriVD  34054  ssralv2VD  34067  truniALTVD  34079  trintALTVD  34081  onfrALTVD  34092  hbimpgVD  34105  ax6e2eqVD  34108  ax6e2ndVD  34109  bj-axd2d  34582