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  2265  axc11r  2370  sb2  2481  mo4  2563  r19.21v  3158  imadifssran  6103  reuop  6245  fundif  6535  tfinds  7796  tfindsg  7797  resf1extb  7870  xpord2indlem  8083  xpord3inddlem  8090  smogt  8293  findcard2  9081  findcard3  9174  fisupg  9179  dffi2  9314  fiinfg  9392  cantnfle  9568  ac5num  9934  pwsdompw  10101  cfsmolem  10168  axcc4  10337  axdc3lem2  10349  fpwwe2lem7  10535  pwfseqlem3  10558  tskord  10678  grudomon  10715  grur1a  10717  xrub  13213  relexprelg  14947  coprmproddvdslem  16575  pcmptcl  16805  restntr  23098  cmpsublem  23315  cmpsub  23316  txlm  23564  ptcmplem3  23970  c1lip1  25930  wilthlem3  27008  dmdbr5  32290  satfsschain  35429  satfrel  35432  satfdm  35434  satffun  35474  antnestlaw1  35756  antnestlaw2  35757  antnestALT  35759  wzel  35887  waj-ax  36479  lukshef-ax2  36480  bj-poni  36610  bj-currypeirce  36622  bj-axd2d  36658  bj-cbvalimt  36704  bj-eximcom  36708  bj-ssbeq  36718  bj-eqs  36740  bj-sbsb  36902  wl-axc11r  37595  finixpnum  37665  mbfresfi  37726  filbcmb  37800  orfa  38142  axc11n-16  39057  axc11-o  39070  unielss  43335  axc5c4c711toc7  44521  axc5c4c711to11  44522  ax6e2nd  44675  elex22VD  44955  exbiriVD  44970  ssralv2VD  44982  truniALTVD  44994  trintALTVD  44996  onfrALTVD  45007  hbimpgVD  45020  ax6e2eqVD  45023  ax6e2ndVD  45024  2reu8i  47237  reupr  47646  reuopreuprim  47650  fmtnofac2lem  47692  sbgoldbwt  47901  sbgoldbst  47902  nnsum4primesodd  47920  nnsum4primesoddALTV  47921  bgoldbnnsum3prm  47928  tgoldbach  47941  gpgprismgr4cycllem2  48220  snlindsntor  48596  itcovalt2  48802