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  800  pm2.26  937  cases2ALT  1046  19.35  1880  19.36imv  1948  axc16g  2252  axc11r  2366  sb2  2480  mo4  2566  r19.21v  3113  r19.35  3271  ab0OLD  4309  reuop  6196  fundif  6483  tfinds  7706  tfindsg  7707  smogt  8198  findcard2  8947  findcard2OLD  9056  findcard3  9057  fisupg  9062  xpfi  9085  dffi2  9182  fiinfg  9258  cantnfle  9429  ac5num  9792  pwsdompw  9960  cfsmolem  10026  axcc4  10195  axdc3lem2  10207  fpwwe2lem7  10393  pwfseqlem3  10416  tskord  10536  grudomon  10573  grur1a  10575  xrub  13046  relexprelg  14749  coprmproddvdslem  16367  pcmptcl  16592  restntr  22333  cmpsublem  22550  cmpsub  22551  txlm  22799  ptcmplem3  23205  c1lip1  25161  wilthlem3  26219  dmdbr5  30670  satfsschain  33326  satfrel  33329  satfdm  33331  satffun  33371  xpord2ind  33794  xpord3ind  33800  wzel  33818  waj-ax  34603  lukshef-ax2  34604  bj-poni  34725  bj-currypeirce  34737  bj-axd2d  34775  bj-cbvalimt  34820  bj-eximcom  34824  bj-ssbeq  34834  bj-eqs  34856  bj-sbsb  35020  wl-axc11r  35689  finixpnum  35762  mbfresfi  35823  filbcmb  35898  orfa  36240  axc11n-16  36952  axc11-o  36965  axc5c4c711toc7  42022  axc5c4c711to11  42023  ax6e2nd  42178  elex22VD  42459  exbiriVD  42474  ssralv2VD  42486  truniALTVD  42498  trintALTVD  42500  onfrALTVD  42511  hbimpgVD  42524  ax6e2eqVD  42527  ax6e2ndVD  42528  2reu8i  44605  reupr  44974  reuopreuprim  44978  fmtnofac2lem  45020  sbgoldbwt  45229  sbgoldbst  45230  nnsum4primesodd  45248  nnsum4primesoddALTV  45249  bgoldbnnsum3prm  45256  tgoldbach  45269  snlindsntor  45812  itcovalt2  46023