Theorem pm2.27 42

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 22	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓))
2	1	com12 32	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  56  com23  86  pm3.2im  160  jcn  162  biimt  360  pm3.35  803  pm2.26  941  cases2ALT  1048  19.35  1874  19.36imv  1942  axc16g  2257  axc11r  2368  sb2  2481  mo4  2563  r19.35OLD  3106  r19.21v  3177  reuop  6314  fundif  6616  tfinds  7880  tfindsg  7881  xpord2indlem  8170  xpord3inddlem  8177  smogt  8405  findcard2  9202  findcard3  9315  findcard3OLD  9316  fisupg  9321  xpfiOLD  9356  dffi2  9460  fiinfg  9536  cantnfle  9708  ac5num  10073  pwsdompw  10240  cfsmolem  10307  axcc4  10476  axdc3lem2  10488  fpwwe2lem7  10674  pwfseqlem3  10697  tskord  10817  grudomon  10854  grur1a  10856  xrub  13350  relexprelg  15073  coprmproddvdslem  16695  pcmptcl  16924  restntr  23205  cmpsublem  23422  cmpsub  23423  txlm  23671  ptcmplem3  24077  c1lip1  26050  wilthlem3  27127  dmdbr5  32336  satfsschain  35348  satfrel  35351  satfdm  35353  satffun  35393  wzel  35805  waj-ax  36396  lukshef-ax2  36397  bj-poni  36527  bj-currypeirce  36539  bj-axd2d  36575  bj-cbvalimt  36621  bj-eximcom  36625  bj-ssbeq  36635  bj-eqs  36657  bj-sbsb  36819  wl-axc11r  37510  finixpnum  37591  mbfresfi  37652  filbcmb  37726  orfa  38068  axc11n-16  38919  axc11-o  38932  unielss  43206  axc5c4c711toc7  44399  axc5c4c711to11  44400  ax6e2nd  44555  elex22VD  44836  exbiriVD  44851  ssralv2VD  44863  truniALTVD  44875  trintALTVD  44877  onfrALTVD  44888  hbimpgVD  44901  ax6e2eqVD  44904  ax6e2ndVD  44905  2reu8i  47062  reupr  47446  reuopreuprim  47450  fmtnofac2lem  47492  sbgoldbwt  47701  sbgoldbst  47702  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  bgoldbnnsum3prm  47728  tgoldbach  47741  snlindsntor  48316  itcovalt2  48526