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  replem  5223  imadifssran  6109  reuop  6251  fundif  6541  tfinds  7804  tfindsg  7805  resf1extb  7878  xpord2indlem  8090  xpord3inddlem  8097  smogt  8300  findcard2  9092  findcard3  9186  fisupg  9191  dffi2  9329  fiinfg  9407  cantnfle  9583  ac5num  9949  pwsdompw  10116  cfsmolem  10183  axcc4  10352  axdc3lem2  10364  fpwwe2lem7  10551  pwfseqlem3  10574  tskord  10694  grudomon  10731  grur1a  10733  xrub  13255  relexprelg  14991  coprmproddvdslem  16622  pcmptcl  16853  restntr  23157  cmpsublem  23374  cmpsub  23375  txlm  23623  ptcmplem3  24029  c1lip1  25974  wilthlem3  27047  oldfib  28383  dmdbr5  32394  satfsschain  35562  satfrel  35565  satfdm  35567  satffun  35607  antnestlaw1  35889  antnestlaw2  35890  antnestALT  35892  wzel  36020  waj-ax  36612  lukshef-ax2  36613  bj-poni  36821  bj-currypeirce  36837  bj-axd2d  36874  bj-eximcom  36927  bj-alextruim  36947  bj-ssbeq  36963  bj-eqs  36986  bj-sbsb  37160  wl-axc11r  37869  finixpnum  37940  mbfresfi  38001  filbcmb  38075  orfa  38417  axc11n-16  39398  axc11-o  39411  unielss  43664  axc5c4c711toc7  44849  axc5c4c711to11  44850  ax6e2nd  45003  elex22VD  45283  exbiriVD  45298  ssralv2VD  45310  truniALTVD  45322  trintALTVD  45324  onfrALTVD  45335  hbimpgVD  45348  ax6e2eqVD  45351  ax6e2ndVD  45352  2reu8i  47573  reupr  47994  reuopreuprim  47998  fmtnofac2lem  48043  sbgoldbwt  48265  sbgoldbst  48266  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  bgoldbnnsum3prm  48292  tgoldbach  48305  gpgprismgr4cycllem2  48584  snlindsntor  48959  itcovalt2  49165