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  802  pm2.26  941  cases2ALT  1048  19.35  1878  19.36imv  1946  axc16g  2263  axc11r  2368  sb2  2479  mo4  2561  r19.21v  3157  imadifssran  6098  reuop  6240  fundif  6530  tfinds  7790  tfindsg  7791  resf1extb  7864  xpord2indlem  8077  xpord3inddlem  8084  smogt  8287  findcard2  9074  findcard3  9167  fisupg  9172  dffi2  9307  fiinfg  9385  cantnfle  9561  ac5num  9924  pwsdompw  10091  cfsmolem  10158  axcc4  10327  axdc3lem2  10339  fpwwe2lem7  10525  pwfseqlem3  10548  tskord  10668  grudomon  10705  grur1a  10707  xrub  13208  relexprelg  14942  coprmproddvdslem  16570  pcmptcl  16800  restntr  23095  cmpsublem  23312  cmpsub  23313  txlm  23561  ptcmplem3  23967  c1lip1  25927  wilthlem3  27005  dmdbr5  32283  satfsschain  35396  satfrel  35399  satfdm  35401  satffun  35441  antnestlaw1  35723  antnestlaw2  35724  antnestALT  35726  wzel  35857  waj-ax  36447  lukshef-ax2  36448  bj-poni  36578  bj-currypeirce  36590  bj-axd2d  36626  bj-cbvalimt  36672  bj-eximcom  36676  bj-ssbeq  36686  bj-eqs  36708  bj-sbsb  36870  wl-axc11r  37563  finixpnum  37644  mbfresfi  37705  filbcmb  37779  orfa  38121  axc11n-16  38976  axc11-o  38989  unielss  43250  axc5c4c711toc7  44436  axc5c4c711to11  44437  ax6e2nd  44590  elex22VD  44870  exbiriVD  44885  ssralv2VD  44897  truniALTVD  44909  trintALTVD  44911  onfrALTVD  44922  hbimpgVD  44935  ax6e2eqVD  44938  ax6e2ndVD  44939  2reu8i  47143  reupr  47552  reuopreuprim  47556  fmtnofac2lem  47598  sbgoldbwt  47807  sbgoldbst  47808  nnsum4primesodd  47826  nnsum4primesoddALTV  47827  bgoldbnnsum3prm  47834  tgoldbach  47847  gpgprismgr4cycllem2  48126  snlindsntor  48502  itcovalt2  48708