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  2296  axc11r  2399  sb2  2510  mo4  2593  r19.21v  3189  replem  5247  imadifssran  6201  imadifssranOLD  6202  reuop  6295  fundif  6586  tfinds  7860  tfindsg  7861  resf1extb  7935  xpord2indlem  8149  xpord3inddlem  8156  smogt  8360  findcard2  9163  findcard3  9257  fisupg  9262  dffi2  9397  fiinfg  9475  cantnfle  9654  ac5num  10043  pwsdompw  10209  cfsmolem  10276  axcc4  10445  axdc3lem2  10457  fpwwe2lem7  10650  pwfseqlem3  10673  tskord  10793  grudomon  10830  grur1a  10832  xrub  13368  relexprelg  15115  coprmproddvdslem  16758  pcmptcl  16989  restntr  23413  cmpsublem  23630  cmpsub  23631  txlm  23880  ptcmplem3  24286  c1lip1  26231  wilthlem3  27314  oldfib  28650  dmdbr5  32797  satfsschain  35951  satfrel  35954  satfdm  35956  satffun  35996  antnestlaw1  36278  antnestlaw2  36279  antnestALT  36281  wzel  36409  waj-ax  37041  lukshef-ax2  37042  bj-poni  37249  bj-currypeirce  37265  bj-axd2d  37302  bj-eximcom  37355  bj-alextruim  37375  bj-ssbeq  37391  bj-eqs  37414  bj-sbsb  37588  wl-axc11r  38301  finixpnum  38367  mbfresfi  38423  filbcmb  38498  orfa  38840  axc11n-16  39819  axc11-o  39832  unielss  44067  axc5c4c711toc7  45236  axc5c4c711to11  45237  ax6e2nd  45389  elex22VD  45669  exbiriVD  45684  ssralv2VD  45696  truniALTVD  45708  trintALTVD  45710  onfrALTVD  45721  hbimpgVD  45734  ax6e2eqVD  45737  ax6e2ndVD  45738  2reu8i  48009  reupr  48430  reuopreuprim  48434  fmtnofac2lem  48479  sbgoldbwt  48701  sbgoldbst  48702  nnsum4primesodd  48720  nnsum4primesoddALTV  48721  bgoldbnnsum3prm  48728  tgoldbach  48741  gpgprismgr4cycllem2  49020  snlindsntor  49409  itcovalt2  49615