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  1878  19.36imv  1946  axc16g  2267  axc11r  2372  sb2  2483  mo4  2566  r19.21v  3161  imadifssran  6109  reuop  6251  fundif  6541  tfinds  7802  tfindsg  7803  resf1extb  7876  xpord2indlem  8089  xpord3inddlem  8096  smogt  8299  findcard2  9089  findcard3  9183  fisupg  9188  dffi2  9326  fiinfg  9404  cantnfle  9580  ac5num  9946  pwsdompw  10113  cfsmolem  10180  axcc4  10349  axdc3lem2  10361  fpwwe2lem7  10548  pwfseqlem3  10571  tskord  10691  grudomon  10728  grur1a  10730  xrub  13227  relexprelg  14961  coprmproddvdslem  16589  pcmptcl  16819  restntr  23126  cmpsublem  23343  cmpsub  23344  txlm  23592  ptcmplem3  23998  c1lip1  25958  wilthlem3  27036  oldfib  28373  dmdbr5  32383  satfsschain  35558  satfrel  35561  satfdm  35563  satffun  35603  antnestlaw1  35885  antnestlaw2  35886  antnestALT  35888  wzel  36016  waj-ax  36608  lukshef-ax2  36609  bj-poni  36745  bj-currypeirce  36757  bj-axd2d  36793  bj-cbvalimt  36839  bj-eximcom  36843  bj-ssbeq  36854  bj-eqs  36876  bj-sbsb  37038  wl-axc11r  37731  finixpnum  37802  mbfresfi  37863  filbcmb  37937  orfa  38279  axc11n-16  39194  axc11-o  39207  unielss  43456  axc5c4c711toc7  44641  axc5c4c711to11  44642  ax6e2nd  44795  elex22VD  45075  exbiriVD  45090  ssralv2VD  45102  truniALTVD  45114  trintALTVD  45116  onfrALTVD  45127  hbimpgVD  45140  ax6e2eqVD  45143  ax6e2ndVD  45144  2reu8i  47355  reupr  47764  reuopreuprim  47768  fmtnofac2lem  47810  sbgoldbwt  48019  sbgoldbst  48020  nnsum4primesodd  48038  nnsum4primesoddALTV  48039  bgoldbnnsum3prm  48046  tgoldbach  48059  gpgprismgr4cycllem2  48338  snlindsntor  48713  itcovalt2  48919