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  2366  sb2  2477  mo4  2559  r19.35OLD  3089  r19.21v  3158  imadifssran  6124  reuop  6266  fundif  6565  tfinds  7836  tfindsg  7837  resf1extb  7910  xpord2indlem  8126  xpord3inddlem  8133  smogt  8336  findcard2  9128  findcard3  9229  findcard3OLD  9230  fisupg  9235  xpfiOLD  9270  dffi2  9374  fiinfg  9452  cantnfle  9624  ac5num  9989  pwsdompw  10156  cfsmolem  10223  axcc4  10392  axdc3lem2  10404  fpwwe2lem7  10590  pwfseqlem3  10613  tskord  10733  grudomon  10770  grur1a  10772  xrub  13272  relexprelg  15004  coprmproddvdslem  16632  pcmptcl  16862  restntr  23069  cmpsublem  23286  cmpsub  23287  txlm  23535  ptcmplem3  23941  c1lip1  25902  wilthlem3  26980  dmdbr5  32237  satfsschain  35351  satfrel  35354  satfdm  35356  satffun  35396  antnestlaw1  35678  antnestlaw2  35679  antnestALT  35681  wzel  35812  waj-ax  36402  lukshef-ax2  36403  bj-poni  36533  bj-currypeirce  36545  bj-axd2d  36581  bj-cbvalimt  36627  bj-eximcom  36631  bj-ssbeq  36641  bj-eqs  36663  bj-sbsb  36825  wl-axc11r  37518  finixpnum  37599  mbfresfi  37660  filbcmb  37734  orfa  38076  axc11n-16  38931  axc11-o  38944  unielss  43207  axc5c4c711toc7  44393  axc5c4c711to11  44394  ax6e2nd  44548  elex22VD  44828  exbiriVD  44843  ssralv2VD  44855  truniALTVD  44867  trintALTVD  44869  onfrALTVD  44880  hbimpgVD  44893  ax6e2eqVD  44896  ax6e2ndVD  44897  2reu8i  47111  reupr  47520  reuopreuprim  47524  fmtnofac2lem  47566  sbgoldbwt  47775  sbgoldbst  47776  nnsum4primesodd  47794  nnsum4primesoddALTV  47795  bgoldbnnsum3prm  47802  tgoldbach  47815  gpgprismgr4cycllem2  48083  snlindsntor  48457  itcovalt2  48663