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  2299  axc11r  2403  sb2  2514  mo4  2597  r19.21v  3193  replem  5254  imadifssran  6207  imadifssranOLD  6208  reuop  6301  fundif  6592  tfinds  7865  tfindsg  7866  resf1extb  7940  xpord2indlem  8152  xpord3inddlem  8159  smogt  8363  findcard2  9159  findcard3  9253  fisupg  9258  dffi2  9393  fiinfg  9471  cantnfle  9650  ac5num  10039  pwsdompw  10205  cfsmolem  10272  axcc4  10441  axdc3lem2  10453  fpwwe2lem7  10640  pwfseqlem3  10663  tskord  10783  grudomon  10820  grur1a  10822  xrub  13356  relexprelg  15101  coprmproddvdslem  16745  pcmptcl  16976  restntr  23376  cmpsublem  23593  cmpsub  23594  txlm  23842  ptcmplem3  24248  c1lip1  26193  wilthlem3  27271  oldfib  28607  dmdbr5  32697  satfsschain  35877  satfrel  35880  satfdm  35882  satffun  35922  antnestlaw1  36204  antnestlaw2  36205  antnestALT  36207  wzel  36335  waj-ax  36966  lukshef-ax2  36967  bj-poni  37174  bj-currypeirce  37190  bj-axd2d  37227  bj-eximcom  37280  bj-alextruim  37300  bj-ssbeq  37316  bj-eqs  37339  bj-sbsb  37513  wl-axc11r  38226  finixpnum  38297  mbfresfi  38358  filbcmb  38432  orfa  38774  axc11n-16  39753  axc11-o  39766  unielss  43986  axc5c4c711toc7  45155  axc5c4c711to11  45156  ax6e2nd  45308  elex22VD  45588  exbiriVD  45603  ssralv2VD  45615  truniALTVD  45627  trintALTVD  45629  onfrALTVD  45640  hbimpgVD  45653  ax6e2eqVD  45656  ax6e2ndVD  45657  2reu8i  47891  reupr  48312  reuopreuprim  48316  fmtnofac2lem  48361  sbgoldbwt  48583  sbgoldbst  48584  nnsum4primesodd  48602  nnsum4primesoddALTV  48603  bgoldbnnsum3prm  48610  tgoldbach  48623  gpgprismgr4cycllem2  48902  snlindsntor  49292  itcovalt2  49498