Theorem pm2.27 41

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 23	. 2 |- ( ( ph -> ps ) -> ( ph -> ps ) )
2	1	com12 33	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  54  com23  82  pm3.2im  149  mth8  150  biimt  337  pm3.35  590  a2andOLD  820  pm2.26  892  cases2  981  19.35  1733  axc112  1994  issref  5230  tfinds  6698  tfindsg  6699  smogt  7092  findcard2  7815  findcard3  7818  fisupg  7823  xpfi  7846  dffi2  7941  fiinfg  8019  cantnfle  8179  ac5num  8469  pwsdompw  8636  cfsmolem  8702  axcc4  8871  axdc3lem2  8883  fpwwe2lem8  9064  pwfseqlem3  9087  tskord  9207  grudomon  9244  grur1a  9246  xrub  11599  relexprelg  13095  coprmproddvdslem  14672  pcmptcl  14829  restntr  20190  cmpsublem  20406  cmpsub  20407  txlm  20655  ptcmplem3  21061  c1lip1  22941  wilthlem3  23987  dmdbr5  27953  wzel  30508  waj-ax  31073  lukshef-ax2  31074  bj-axd2d  31174  finixpnum  31888  mbfresfi  31945  filbcmb  32025  orfa  32273  axc11n-16  32472  axc11-o  32485  axc5c4c711toc7  36657  axc5c4c711to11  36658  ax6e2nd  36827  elex22VD  37140  exbiriVD  37155  ssralv2VD  37168  truniALTVD  37180  trintALTVD  37182  onfrALTVD  37193  hbimpgVD  37206  ax6e2eqVD  37209  ax6e2ndVD  37210  bgoldbwt  38634  bgoldbst  38635  nnsum4primesodd  38647  nnsum4primesoddALTV  38648  bgoldbnnsum3prm  38655  tgoldbach  38667  snlindsntor  39608