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  362  pm3.35  812  pm2.26  952  cases2ALT  1059  19.35  1896  19.36imv  1964  axc16g  2294  axc11r  2398  sb2  2509  mo4  2592  r19.21v  3186  replem  5237  imadifssran  6133  reuop  6276  fundif  6566  tfinds  7836  tfindsg  7837  resf1extb  7911  xpord2indlem  8122  xpord3inddlem  8129  smogt  8333  findcard2  9129  findcard3  9223  fisupg  9228  dffi2  9366  fiinfg  9444  cantnfle  9623  ac5num  9989  pwsdompw  10156  cfsmolem  10224  axcc4  10393  axdc3lem2  10405  fpwwe2lem7  10592  pwfseqlem3  10615  tskord  10735  grudomon  10772  grur1a  10774  xrub  13312  relexprelg  15048  coprmproddvdslem  16679  pcmptcl  16910  restntr  23222  cmpsublem  23439  cmpsub  23440  txlm  23688  ptcmplem3  24094  c1lip1  26039  wilthlem3  27111  oldfib  28447  dmdbr5  32457  satfsschain  35678  satfrel  35681  satfdm  35683  satffun  35723  antnestlaw1  36005  antnestlaw2  36006  antnestALT  36008  wzel  36136  waj-ax  36738  lukshef-ax2  36739  bj-poni  36947  bj-currypeirce  36963  bj-axd2d  37000  bj-eximcom  37053  bj-alextruim  37073  bj-ssbeq  37089  bj-eqs  37112  bj-sbsb  37286  wl-axc11r  37997  finixpnum  38068  mbfresfi  38129  filbcmb  38203  orfa  38545  axc11n-16  39526  axc11-o  39539  unielss  43759  axc5c4c711toc7  44944  axc5c4c711to11  44945  ax6e2nd  45098  elex22VD  45378  exbiriVD  45393  ssralv2VD  45405  truniALTVD  45417  trintALTVD  45419  onfrALTVD  45430  hbimpgVD  45443  ax6e2eqVD  45446  ax6e2ndVD  45447  2reu8i  47671  reupr  48092  reuopreuprim  48096  fmtnofac2lem  48141  sbgoldbwt  48363  sbgoldbst  48364  nnsum4primesodd  48382  nnsum4primesoddALTV  48383  bgoldbnnsum3prm  48390  tgoldbach  48403  gpgprismgr4cycllem2  48682  snlindsntor  49057  itcovalt2  49263