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  801  pm2.26  938  cases2ALT  1047  19.35  1880  19.36imv  1948  axc16g  2251  axc11r  2364  sb2  2477  mo4  2559  r19.35OLD  3108  r19.21v  3172  ab0OLD  4340  reuop  6250  fundif  6555  tfinds  7801  tfindsg  7802  xpord2indlem  8084  xpord3inddlem  8091  smogt  8318  findcard2  9115  findcard2OLD  9235  findcard3  9236  findcard3OLD  9237  fisupg  9242  xpfiOLD  9269  dffi2  9368  fiinfg  9444  cantnfle  9616  ac5num  9981  pwsdompw  10149  cfsmolem  10215  axcc4  10384  axdc3lem2  10396  fpwwe2lem7  10582  pwfseqlem3  10605  tskord  10725  grudomon  10762  grur1a  10764  xrub  13241  relexprelg  14935  coprmproddvdslem  16549  pcmptcl  16774  restntr  22570  cmpsublem  22787  cmpsub  22788  txlm  23036  ptcmplem3  23442  c1lip1  25398  wilthlem3  26456  dmdbr5  31313  satfsschain  34045  satfrel  34048  satfdm  34050  satffun  34090  wzel  34485  waj-ax  34962  lukshef-ax2  34963  bj-poni  35084  bj-currypeirce  35096  bj-axd2d  35134  bj-cbvalimt  35179  bj-eximcom  35183  bj-ssbeq  35193  bj-eqs  35215  bj-sbsb  35378  wl-axc11r  36062  finixpnum  36136  mbfresfi  36197  filbcmb  36272  orfa  36614  axc11n-16  37473  axc11-o  37486  unielss  41610  axc5c4c711toc7  42806  axc5c4c711to11  42807  ax6e2nd  42962  elex22VD  43243  exbiriVD  43258  ssralv2VD  43270  truniALTVD  43282  trintALTVD  43284  onfrALTVD  43295  hbimpgVD  43308  ax6e2eqVD  43311  ax6e2ndVD  43312  2reu8i  45465  reupr  45834  reuopreuprim  45838  fmtnofac2lem  45880  sbgoldbwt  46089  sbgoldbst  46090  nnsum4primesodd  46108  nnsum4primesoddALTV  46109  bgoldbnnsum3prm  46116  tgoldbach  46129  snlindsntor  46672  itcovalt2  46883