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 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))

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  57  com23  87  pm3.2im  161  jcn  163  biimt  363  pm3.35  814  pm2.26  954  cases2ALT  1062  19.35  1904  19.36imv  1972  axc16g  2302  axc11r  2406  sb2  2517  mo4  2600  r19.21v  3196  replem  5251  imadifssran  6203  imadifssranOLD  6204  reuop  6295  fundif  6586  tfinds  7856  tfindsg  7857  resf1extb  7931  xpord2indlem  8143  xpord3inddlem  8150  smogt  8354  findcard2  9149  findcard3  9243  fisupg  9248  dffi2  9383  fiinfg  9461  cantnfle  9640  ac5num  10020  pwsdompw  10186  cfsmolem  10254  axcc4  10423  axdc3lem2  10435  fpwwe2lem7  10622  pwfseqlem3  10645  tskord  10765  grudomon  10802  grur1a  10804  xrub  13338  relexprelg  15075  coprmproddvdslem  16720  pcmptcl  16951  restntr  23308  cmpsublem  23525  cmpsub  23526  txlm  23774  ptcmplem3  24180  c1lip1  26125  wilthlem3  27200  oldfib  28536  dmdbr5  32601  satfsschain  35789  satfrel  35792  satfdm  35794  satffun  35834  antnestlaw1  36116  antnestlaw2  36117  antnestALT  36119  wzel  36247  waj-ax  36848  lukshef-ax2  36849  bj-poni  37056  bj-currypeirce  37072  bj-axd2d  37109  bj-eximcom  37162  bj-alextruim  37182  bj-ssbeq  37198  bj-eqs  37221  bj-sbsb  37395  wl-axc11r  38108  finixpnum  38179  mbfresfi  38240  filbcmb  38314  orfa  38656  axc11n-16  39637  axc11-o  39650  unielss  43872  axc5c4c711toc7  45041  axc5c4c711to11  45042  ax6e2nd  45194  elex22VD  45474  exbiriVD  45489  ssralv2VD  45501  truniALTVD  45513  trintALTVD  45515  onfrALTVD  45526  hbimpgVD  45539  ax6e2eqVD  45542  ax6e2ndVD  45543  2reu8i  47774  reupr  48195  reuopreuprim  48199  fmtnofac2lem  48244  sbgoldbwt  48466  sbgoldbst  48467  nnsum4primesodd  48485  nnsum4primesoddALTV  48486  bgoldbnnsum3prm  48493  tgoldbach  48506  gpgprismgr4cycllem2  48785  snlindsntor  49171  itcovalt2  49377