Theorem pm2.27 43

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 23	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓))
2	1	com12 33	1 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  pm2.43  57  com23  87  pm3.2im  161  jcn  163  biimt  363  pm3.35  815  pm2.26  954  cases2ALT  1064  19.35  1910  19.36imv  1978  axc16g  2295  axc11r  2398  sb2  2509  mo4  2592  r19.21v  3188  replem  5241  imadifssran  6195  imadifssranOLD  6196  reuop  6289  fundif  6581  tfinds  7860  tfindsg  7861  resf1extb  7935  xpord2indlem  8148  xpord3inddlem  8155  smogt  8359  findcard2  9164  findcard3  9258  fisupg  9263  dffi2  9399  fiinfg  9477  cantnfle  9656  ac5num  10096  pwsdompw  10262  cfsmolem  10329  axcc4  10498  axdc3lem2  10510  fpwwe2lem7  10703  pwfseqlem3  10726  tskord  10846  grudomon  10883  grur1a  10885  xrub  13423  relexprelg  15171  coprmproddvdslem  16817  pcmptcl  17049  restntr  23480  cmpsublem  23697  cmpsub  23698  txlm  23947  ptcmplem3  24353  c1lip1  26297  wilthlem3  27379  fltoprm  27977  fltoprmgt3  27978  oldfib  28745  dmdbr5  32892  satfsschain  36098  satfrel  36101  satfdm  36103  satffun  36143  antnestlaw1  36425  antnestlaw2  36426  antnestALT  36428  wzel  36556  waj-ax  37172  lukshef-ax2  37173  bj-poni  37380  bj-currypeirce  37396  bj-axd2d  37433  bj-eximcom  37486  bj-alextruim  37506  bj-ssbeq  37522  bj-eqs  37545  bj-sbsb  37719  wl-axc11r  38430  finixpnum  38496  mbfresfi  38552  filbcmb  38642  orfa  38984  axc11n-16  39963  axc11-o  39976  unielss  44178  axc5c4c711toc7  45347  axc5c4c711to11  45348  ax6e2nd  45500  elex22VD  45780  exbiriVD  45795  ssralv2VD  45807  truniALTVD  45819  trintALTVD  45821  onfrALTVD  45832  hbimpgVD  45845  ax6e2eqVD  45848  ax6e2ndVD  45849  2reu8i  48127  reupr  48548  reuopreuprim  48552  fmtnofac2lem  48597  sbgoldbwt  48819  sbgoldbst  48820  nnsum4primesodd  48838  nnsum4primesoddALTV  48839  bgoldbnnsum3prm  48846  tgoldbach  48859  gpgprismgr4cycllem2  49138  snlindsntor  49527  itcovalt2  49733