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, 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 32	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  81  pm3.2im  149  mth8  150  biimt  337  pm3.35  591  a2andOLD  821  pm2.26  894  cases2  983  19.35  1740  axc112  2020  issref  5213  tfinds  6686  tfindsg  6687  smogt  7086  findcard2  7811  findcard3  7814  fisupg  7819  xpfi  7842  dffi2  7937  fiinfg  8015  cantnfle  8176  ac5num  8467  pwsdompw  8634  cfsmolem  8700  axcc4  8869  axdc3lem2  8881  fpwwe2lem8  9062  pwfseqlem3  9085  tskord  9205  grudomon  9242  grur1a  9244  xrub  11597  relexprelg  13101  coprmproddvdslem  14679  pcmptcl  14836  restntr  20198  cmpsublem  20414  cmpsub  20415  txlm  20663  ptcmplem3  21069  c1lip1  22949  wilthlem3  23995  dmdbr5  27961  wzel  30507  waj-ax  31074  lukshef-ax2  31075  bj-axd2d  31176  bj-sbex  31239  bj-ssbeq  31240  bj-ssb0  31241  finixpnum  31930  mbfresfi  31987  filbcmb  32067  orfa  32315  axc11n-16  32509  axc11-o  32522  axc5c4c711toc7  36755  axc5c4c711to11  36756  ax6e2nd  36925  elex22VD  37235  exbiriVD  37250  ssralv2VD  37263  truniALTVD  37275  trintALTVD  37277  onfrALTVD  37288  hbimpgVD  37301  ax6e2eqVD  37304  ax6e2ndVD  37305  bgoldbwt  38878  bgoldbst  38879  nnsum4primesodd  38891  nnsum4primesoddALTV  38892  bgoldbnnsum3prm  38899  tgoldbach  38911  snlindsntor  40317