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  1909  19.36imv  1977  axc16g  2294  axc11r  2397  sb2  2508  mo4  2591  r19.21v  3187  replem  5240  imadifssranOLD  6202  imadifssranOLDOLD  6203  reuop  6296  fundif  6589  tfinds  7871  tfindsg  7872  resf1extb  7946  xpord2indlem  8166  xpord3inddlem  8173  smogt  8378  findcard2  9183  findcard3  9277  fisupg  9282  dffi2  9418  fiinfg  9496  cantnfle  9675  ac5num  10118  pwsdompw  10284  cfsmolem  10351  axcc4  10520  axdc3lem2  10532  fpwwe2lem7  10725  pwfseqlem3  10748  tskord  10868  grudomon  10905  grur1a  10907  xrub  13445  relexprelg  15196  coprmproddvdslem  16842  pcmptcl  17074  restntr  23505  cmpsublem  23722  cmpsub  23723  txlm  23972  ptcmplem3  24378  c1lip1  26322  wilthlem3  27402  fltoprm  28000  fltoprmgt3  28001  oldfib  28768  dmdbr5  32915  onprcf1acwevdlem1  35964  satfsschain  36215  satfrel  36218  satfdm  36220  satffun  36260  antnestlaw1  36542  antnestlaw2  36543  antnestALT  36545  wzel  36678  waj-ax  37294  lukshef-ax2  37295  bj-poni  37502  bj-currypeirce  37518  bj-axd2d  37555  bj-eximcom  37608  bj-alextruim  37628  bj-ssbeq  37644  bj-eqs  37667  bj-sbsb  37841  wl-axc11r  38555  finixpnum  38621  mbfresfi  38677  filbcmb  38767  orfa  39109  axc11n-16  40088  axc11-o  40101  unielss  44313  axc5c4c711toc7  45481  axc5c4c711to11  45482  ax6e2nd  45634  elex22VD  45914  exbiriVD  45929  ssralv2VD  45941  truniALTVD  45953  trintALTVD  45955  onfrALTVD  45966  hbimpgVD  45979  ax6e2eqVD  45982  ax6e2ndVD  45983  2reu8i  48276  reupr  48697  reuopreuprim  48701  fmtnofac2lem  48746  sbgoldbwt  48968  sbgoldbst  48969  nnsum4primesodd  48987  nnsum4primesoddALTV  48988  bgoldbnnsum3prm  48995  tgoldbach  49008  gpgprismgr4cycllem2  49287  snlindsntor  49676  itcovalt2  49882