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  162  jcn  164  biimt  363  pm3.35  801  pm2.26  936  cases2ALT  1043  19.35  1874  spsbeOLD  2085  axc16g  2256  axc11r  2382  sb2  2500  mo4  2646  r19.35  3341  reuop  6139  fundif  6398  tfinds  7568  tfindsg  7569  smogt  7998  findcard2  8752  findcard3  8755  fisupg  8760  xpfi  8783  dffi2  8881  fiinfg  8957  cantnfle  9128  ac5num  9456  pwsdompw  9620  cfsmolem  9686  axcc4  9855  axdc3lem2  9867  fpwwe2lem8  10053  pwfseqlem3  10076  tskord  10196  grudomon  10233  grur1a  10235  xrub  12699  relexprelg  14391  coprmproddvdslem  16000  pcmptcl  16221  restntr  21784  cmpsublem  22001  cmpsub  22002  txlm  22250  ptcmplem3  22656  c1lip1  24588  wilthlem3  25641  dmdbr5  30079  satfsschain  32606  satfrel  32609  satfdm  32611  satffun  32651  wzel  33106  waj-ax  33757  lukshef-ax2  33758  bj-currypeirce  33887  bj-axd2d  33922  bj-cbvalimt  33967  bj-eximcom  33971  bj-ssbeq  33981  bj-eqs  34003  bj-sbsb  34155  wl-axc11r  34764  finixpnum  34871  mbfresfi  34932  filbcmb  35009  orfa  35354  axc11n-16  36068  axc11-o  36081  axc5c4c711toc7  40729  axc5c4c711to11  40730  ax6e2nd  40885  elex22VD  41166  exbiriVD  41181  ssralv2VD  41193  truniALTVD  41205  trintALTVD  41207  onfrALTVD  41218  hbimpgVD  41231  ax6e2eqVD  41234  ax6e2ndVD  41235  2reu8i  43305  reupr  43677  reuopreuprim  43681  fmtnofac2lem  43723  sbgoldbwt  43935  sbgoldbst  43936  nnsum4primesodd  43954  nnsum4primesoddALTV  43955  bgoldbnnsum3prm  43962  tgoldbach  43975  snlindsntor  44519