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  1879  19.36imv  1947  axc16g  2268  axc11r  2373  sb2  2484  mo4  2567  r19.21v  3163  imadifssran  6117  reuop  6259  fundif  6549  tfinds  7812  tfindsg  7813  resf1extb  7886  xpord2indlem  8099  xpord3inddlem  8106  smogt  8309  findcard2  9101  findcard3  9195  fisupg  9200  dffi2  9338  fiinfg  9416  cantnfle  9592  ac5num  9958  pwsdompw  10125  cfsmolem  10192  axcc4  10361  axdc3lem2  10373  fpwwe2lem7  10560  pwfseqlem3  10583  tskord  10703  grudomon  10740  grur1a  10742  xrub  13239  relexprelg  14973  coprmproddvdslem  16601  pcmptcl  16831  restntr  23138  cmpsublem  23355  cmpsub  23356  txlm  23604  ptcmplem3  24010  c1lip1  25970  wilthlem3  27048  oldfib  28385  dmdbr5  32395  satfsschain  35577  satfrel  35580  satfdm  35582  satffun  35622  antnestlaw1  35904  antnestlaw2  35905  antnestALT  35907  wzel  36035  waj-ax  36627  lukshef-ax2  36628  bj-poni  36764  bj-currypeirce  36778  bj-axd2d  36814  bj-cbvalimt  36869  bj-eximcom  36871  bj-alextruim  36874  bj-ssbeq  36892  bj-eqs  36914  bj-sbsb  37079  wl-axc11r  37779  finixpnum  37850  mbfresfi  37911  filbcmb  37985  orfa  38327  axc11n-16  39308  axc11-o  39321  unielss  43569  axc5c4c711toc7  44754  axc5c4c711to11  44755  ax6e2nd  44908  elex22VD  45188  exbiriVD  45203  ssralv2VD  45215  truniALTVD  45227  trintALTVD  45229  onfrALTVD  45240  hbimpgVD  45253  ax6e2eqVD  45256  ax6e2ndVD  45257  2reu8i  47467  reupr  47876  reuopreuprim  47880  fmtnofac2lem  47922  sbgoldbwt  48131  sbgoldbst  48132  nnsum4primesodd  48150  nnsum4primesoddALTV  48151  bgoldbnnsum3prm  48158  tgoldbach  48171  gpgprismgr4cycllem2  48450  snlindsntor  48825  itcovalt2  49031