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  1877  19.36imv  1945  axc16g  2261  axc11r  2366  sb2  2477  mo4  2559  r19.21v  3154  imadifssran  6104  reuop  6245  fundif  6535  tfinds  7800  tfindsg  7801  resf1extb  7874  xpord2indlem  8087  xpord3inddlem  8094  smogt  8297  findcard2  9088  findcard3  9187  findcard3OLD  9188  fisupg  9193  xpfiOLD  9228  dffi2  9332  fiinfg  9410  cantnfle  9586  ac5num  9949  pwsdompw  10116  cfsmolem  10183  axcc4  10352  axdc3lem2  10364  fpwwe2lem7  10550  pwfseqlem3  10573  tskord  10693  grudomon  10730  grur1a  10732  xrub  13232  relexprelg  14963  coprmproddvdslem  16591  pcmptcl  16821  restntr  23085  cmpsublem  23302  cmpsub  23303  txlm  23551  ptcmplem3  23957  c1lip1  25918  wilthlem3  26996  dmdbr5  32270  satfsschain  35336  satfrel  35339  satfdm  35341  satffun  35381  antnestlaw1  35663  antnestlaw2  35664  antnestALT  35666  wzel  35797  waj-ax  36387  lukshef-ax2  36388  bj-poni  36518  bj-currypeirce  36530  bj-axd2d  36566  bj-cbvalimt  36612  bj-eximcom  36616  bj-ssbeq  36626  bj-eqs  36648  bj-sbsb  36810  wl-axc11r  37503  finixpnum  37584  mbfresfi  37645  filbcmb  37719  orfa  38061  axc11n-16  38916  axc11-o  38929  unielss  43191  axc5c4c711toc7  44377  axc5c4c711to11  44378  ax6e2nd  44532  elex22VD  44812  exbiriVD  44827  ssralv2VD  44839  truniALTVD  44851  trintALTVD  44853  onfrALTVD  44864  hbimpgVD  44877  ax6e2eqVD  44880  ax6e2ndVD  44881  2reu8i  47098  reupr  47507  reuopreuprim  47511  fmtnofac2lem  47553  sbgoldbwt  47762  sbgoldbst  47763  nnsum4primesodd  47781  nnsum4primesoddALTV  47782  bgoldbnnsum3prm  47789  tgoldbach  47802  gpgprismgr4cycllem2  48081  snlindsntor  48457  itcovalt2  48663