Theorem pm2.27 42

Description: This theorem, sometimes called "Assertion" or "Pon" (for "ponens"), can be thought of as a 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	⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))

Proof of Theorem pm2.27

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓))
2	1	com12 32	1 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))

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  56  com23  86  pm3.2im  160  jcn  162  biimt  361  pm3.35  802  pm2.26  939  cases2ALT  1048  19.35  1881  19.36imv  1949  axc16g  2252  axc11r  2366  sb2  2479  mo4  2561  r19.35OLD  3110  r19.21v  3180  ab0OLD  4376  reuop  6293  fundif  6598  tfinds  7849  tfindsg  7850  xpord2indlem  8133  xpord3inddlem  8140  smogt  8367  findcard2  9164  findcard2OLD  9284  findcard3  9285  findcard3OLD  9286  fisupg  9291  xpfiOLD  9318  dffi2  9418  fiinfg  9494  cantnfle  9666  ac5num  10031  pwsdompw  10199  cfsmolem  10265  axcc4  10434  axdc3lem2  10446  fpwwe2lem7  10632  pwfseqlem3  10655  tskord  10775  grudomon  10812  grur1a  10814  xrub  13291  relexprelg  14985  coprmproddvdslem  16599  pcmptcl  16824  restntr  22686  cmpsublem  22903  cmpsub  22904  txlm  23152  ptcmplem3  23558  c1lip1  25514  wilthlem3  26574  dmdbr5  31592  satfsschain  34386  satfrel  34389  satfdm  34391  satffun  34431  wzel  34827  waj-ax  35347  lukshef-ax2  35348  bj-poni  35469  bj-currypeirce  35481  bj-axd2d  35519  bj-cbvalimt  35564  bj-eximcom  35568  bj-ssbeq  35578  bj-eqs  35600  bj-sbsb  35763  wl-axc11r  36447  finixpnum  36521  mbfresfi  36582  filbcmb  36656  orfa  36998  axc11n-16  37856  axc11-o  37869  unielss  42015  axc5c4c711toc7  43211  axc5c4c711to11  43212  ax6e2nd  43367  elex22VD  43648  exbiriVD  43663  ssralv2VD  43675  truniALTVD  43687  trintALTVD  43689  onfrALTVD  43700  hbimpgVD  43713  ax6e2eqVD  43716  ax6e2ndVD  43717  2reu8i  45869  reupr  46238  reuopreuprim  46242  fmtnofac2lem  46284  sbgoldbwt  46493  sbgoldbst  46494  nnsum4primesodd  46512  nnsum4primesoddALTV  46513  bgoldbnnsum3prm  46520  tgoldbach  46533  snlindsntor  47200  itcovalt2  47411