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  1912  19.36imv  1980  axc16g  2298  axc11r  2400  sb2  2511  mo4  2594  r19.21v  3191  replem  5244  imadifssranOLD  6215  imadifssranOLDOLD  6216  reuop  6314  fundifOLD  6611  tfinds  7895  tfindsg  7896  resf1extb  7970  xpord2indlem  8191  xpord3inddlem  8198  smogt  8403  findcard2  9208  findcard3  9302  fisupg  9307  dffi2  9442  fiinfg  9520  cantnfle  9699  ac5num  10142  pwsdompw  10308  cfsmolem  10375  axcc4  10544  axdc3lem2  10556  fpwwe2lem7  10749  pwfseqlem3  10772  tskord  10892  grudomon  10929  grur1a  10931  xrub  13469  relexprelg  15220  coprmproddvdslem  16866  pcmptcl  17098  restntr  23530  cmpsublem  23747  cmpsub  23748  txlm  23997  ptcmplem3  24403  c1lip1  26347  wilthlem3  27427  fltoprm  28025  fltoprmgt3  28026  oldfib  28793  dmdbr5  32940  onprcf1acwevdlem1  36045  satfsschain  36296  satfrel  36299  satfdm  36301  satffun  36341  antnestlaw1  36623  antnestlaw2  36624  antnestALT  36626  wzel  36764  waj-ax  37380  lukshef-ax2  37381  bj-poni  37588  bj-currypeirce  37604  bj-axd2d  37641  bj-eximcom  37694  bj-alextruim  37714  bj-ssbeq  37730  bj-eqs  37753  bj-sbsb  37927  wl-axc11r  38654  finixpnum  38720  mbfresfi  38776  filbcmb  38866  orfa  39208  axc11n-16  40187  axc11-o  40200  unielss  44412  axc5c4c711toc7  45580  axc5c4c711to11  45581  ax6e2nd  45732  elex22VD  46012  exbiriVD  46027  ssralv2VD  46039  truniALTVD  46051  trintALTVD  46053  onfrALTVD  46064  hbimpgVD  46077  ax6e2eqVD  46080  ax6e2ndVD  46081  2reu8i  48389  reupr  48809  reuopreuprim  48813  fmtnofac2lem  48858  sbgoldbwt  49080  sbgoldbst  49081  nnsum4primesodd  49099  nnsum4primesoddALTV  49100  bgoldbnnsum3prm  49107  tgoldbach  49120  gpgprismgr4cycllem2  49399  snlindsntor  49788  itcovalt2  49994