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  942  cases2ALT  1049  19.35  1877  19.36imv  1945  axc16g  2260  axc11r  2371  sb2  2484  mo4  2566  r19.35OLD  3109  r19.21v  3180  imadifssran  6171  reuop  6313  fundif  6615  tfinds  7881  tfindsg  7882  resf1extb  7956  xpord2indlem  8172  xpord3inddlem  8179  smogt  8407  findcard2  9204  findcard3  9318  findcard3OLD  9319  fisupg  9324  xpfiOLD  9359  dffi2  9463  fiinfg  9539  cantnfle  9711  ac5num  10076  pwsdompw  10243  cfsmolem  10310  axcc4  10479  axdc3lem2  10491  fpwwe2lem7  10677  pwfseqlem3  10700  tskord  10820  grudomon  10857  grur1a  10859  xrub  13354  relexprelg  15077  coprmproddvdslem  16699  pcmptcl  16929  restntr  23190  cmpsublem  23407  cmpsub  23408  txlm  23656  ptcmplem3  24062  c1lip1  26036  wilthlem3  27113  dmdbr5  32327  satfsschain  35369  satfrel  35372  satfdm  35374  satffun  35414  wzel  35825  waj-ax  36415  lukshef-ax2  36416  bj-poni  36546  bj-currypeirce  36558  bj-axd2d  36594  bj-cbvalimt  36640  bj-eximcom  36644  bj-ssbeq  36654  bj-eqs  36676  bj-sbsb  36838  wl-axc11r  37531  finixpnum  37612  mbfresfi  37673  filbcmb  37747  orfa  38089  axc11n-16  38939  axc11-o  38952  unielss  43230  axc5c4c711toc7  44423  axc5c4c711to11  44424  ax6e2nd  44578  elex22VD  44859  exbiriVD  44874  ssralv2VD  44886  truniALTVD  44898  trintALTVD  44900  onfrALTVD  44911  hbimpgVD  44924  ax6e2eqVD  44927  ax6e2ndVD  44928  2reu8i  47125  reupr  47509  reuopreuprim  47513  fmtnofac2lem  47555  sbgoldbwt  47764  sbgoldbst  47765  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  bgoldbnnsum3prm  47791  tgoldbach  47804  snlindsntor  48388  itcovalt2  48598