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  799  pm2.26  936  cases2ALT  1045  19.35  1881  19.36imv  1949  axc16g  2255  axc11r  2366  sb2  2480  mo4  2566  r19.35  3268  ab0OLD  4306  reuop  6185  fundif  6467  tfinds  7681  tfindsg  7682  smogt  8169  findcard2  8909  findcard2OLD  8986  findcard3  8987  fisupg  8992  xpfi  9015  dffi2  9112  fiinfg  9188  cantnfle  9359  ac5num  9723  pwsdompw  9891  cfsmolem  9957  axcc4  10126  axdc3lem2  10138  fpwwe2lem7  10324  pwfseqlem3  10347  tskord  10467  grudomon  10504  grur1a  10506  xrub  12975  relexprelg  14677  coprmproddvdslem  16295  pcmptcl  16520  restntr  22241  cmpsublem  22458  cmpsub  22459  txlm  22707  ptcmplem3  23113  c1lip1  25066  wilthlem3  26124  dmdbr5  30571  satfsschain  33226  satfrel  33229  satfdm  33231  satffun  33271  xpord2ind  33721  xpord3ind  33727  wzel  33745  waj-ax  34530  lukshef-ax2  34531  bj-poni  34652  bj-currypeirce  34664  bj-axd2d  34702  bj-cbvalimt  34747  bj-eximcom  34751  bj-ssbeq  34761  bj-eqs  34783  bj-sbsb  34947  wl-axc11r  35616  finixpnum  35689  mbfresfi  35750  filbcmb  35825  orfa  36167  axc11n-16  36879  axc11-o  36892  axc5c4c711toc7  41911  axc5c4c711to11  41912  ax6e2nd  42067  elex22VD  42348  exbiriVD  42363  ssralv2VD  42375  truniALTVD  42387  trintALTVD  42389  onfrALTVD  42400  hbimpgVD  42413  ax6e2eqVD  42416  ax6e2ndVD  42417  2reu8i  44492  reupr  44862  reuopreuprim  44866  fmtnofac2lem  44908  sbgoldbwt  45117  sbgoldbst  45118  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  bgoldbnnsum3prm  45144  tgoldbach  45157  snlindsntor  45700  itcovalt2  45911