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  163  jcn  165  biimt  364  pm3.35  802  pm2.26  937  cases2ALT  1044  19.35  1878  axc16g  2258  axc11r  2375  sb2  2493  mo4  2625  r19.35  3295  reuop  6112  fundif  6373  tfinds  7554  tfindsg  7555  smogt  7987  findcard2  8742  findcard3  8745  fisupg  8750  xpfi  8773  dffi2  8871  fiinfg  8947  cantnfle  9118  ac5num  9447  pwsdompw  9615  cfsmolem  9681  axcc4  9850  axdc3lem2  9862  fpwwe2lem8  10048  pwfseqlem3  10071  tskord  10191  grudomon  10228  grur1a  10230  xrub  12693  relexprelg  14389  coprmproddvdslem  15996  pcmptcl  16217  restntr  21787  cmpsublem  22004  cmpsub  22005  txlm  22253  ptcmplem3  22659  c1lip1  24600  wilthlem3  25655  dmdbr5  30091  satfsschain  32724  satfrel  32727  satfdm  32729  satffun  32769  wzel  33224  waj-ax  33875  lukshef-ax2  33876  bj-currypeirce  34005  bj-axd2d  34040  bj-cbvalimt  34085  bj-eximcom  34089  bj-ssbeq  34099  bj-eqs  34121  bj-sbsb  34275  wl-axc11r  34935  finixpnum  35042  mbfresfi  35103  filbcmb  35178  orfa  35520  axc11n-16  36234  axc11-o  36247  axc5c4c711toc7  41108  axc5c4c711to11  41109  ax6e2nd  41264  elex22VD  41545  exbiriVD  41560  ssralv2VD  41572  truniALTVD  41584  trintALTVD  41586  onfrALTVD  41597  hbimpgVD  41610  ax6e2eqVD  41613  ax6e2ndVD  41614  2reu8i  43669  reupr  44039  reuopreuprim  44043  fmtnofac2lem  44085  sbgoldbwt  44295  sbgoldbst  44296  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  bgoldbnnsum3prm  44322  tgoldbach  44335  snlindsntor  44880  itcovalt2  45091