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  360  pm3.35  802  pm2.26  941  cases2ALT  1048  19.35  1877  19.36imv  1945  axc16g  2261  axc11r  2371  sb2  2484  mo4  2566  r19.35OLD  3097  r19.21v  3166  imadifssran  6145  reuop  6287  fundif  6590  tfinds  7860  tfindsg  7861  resf1extb  7935  xpord2indlem  8151  xpord3inddlem  8158  smogt  8386  findcard2  9183  findcard3  9295  findcard3OLD  9296  fisupg  9301  xpfiOLD  9336  dffi2  9440  fiinfg  9518  cantnfle  9690  ac5num  10055  pwsdompw  10222  cfsmolem  10289  axcc4  10458  axdc3lem2  10470  fpwwe2lem7  10656  pwfseqlem3  10679  tskord  10799  grudomon  10836  grur1a  10838  xrub  13333  relexprelg  15062  coprmproddvdslem  16686  pcmptcl  16916  restntr  23125  cmpsublem  23342  cmpsub  23343  txlm  23591  ptcmplem3  23997  c1lip1  25959  wilthlem3  27037  dmdbr5  32294  satfsschain  35391  satfrel  35394  satfdm  35396  satffun  35436  wzel  35847  waj-ax  36437  lukshef-ax2  36438  bj-poni  36568  bj-currypeirce  36580  bj-axd2d  36616  bj-cbvalimt  36662  bj-eximcom  36666  bj-ssbeq  36676  bj-eqs  36698  bj-sbsb  36860  wl-axc11r  37553  finixpnum  37634  mbfresfi  37695  filbcmb  37769  orfa  38111  axc11n-16  38961  axc11-o  38974  unielss  43209  axc5c4c711toc7  44395  axc5c4c711to11  44396  ax6e2nd  44550  elex22VD  44830  exbiriVD  44845  ssralv2VD  44857  truniALTVD  44869  trintALTVD  44871  onfrALTVD  44882  hbimpgVD  44895  ax6e2eqVD  44898  ax6e2ndVD  44899  2reu8i  47109  reupr  47503  reuopreuprim  47507  fmtnofac2lem  47549  sbgoldbwt  47758  sbgoldbst  47759  nnsum4primesodd  47777  nnsum4primesoddALTV  47778  bgoldbnnsum3prm  47785  tgoldbach  47798  gpgprismgr4cycllem2  48062  snlindsntor  48414  itcovalt2  48624