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  803  pm2.26  939  cases2ALT  1048  19.35  1884  19.36imv  1952  axc16g  2261  axc11r  2369  sb2  2481  mo4  2567  r19.35  3247  ab0OLD  4265  reuop  6126  fundif  6389  tfinds  7596  tfindsg  7597  smogt  8036  findcard2  8766  findcard2OLD  8837  findcard3  8838  fisupg  8843  xpfi  8866  dffi2  8963  fiinfg  9039  cantnfle  9210  ac5num  9539  pwsdompw  9707  cfsmolem  9773  axcc4  9942  axdc3lem2  9954  fpwwe2lem7  10140  pwfseqlem3  10163  tskord  10283  grudomon  10320  grur1a  10322  xrub  12791  relexprelg  14490  coprmproddvdslem  16106  pcmptcl  16330  restntr  21936  cmpsublem  22153  cmpsub  22154  txlm  22402  ptcmplem3  22808  c1lip1  24752  wilthlem3  25810  dmdbr5  30246  satfsschain  32900  satfrel  32903  satfdm  32905  satffun  32945  xpord2ind  33410  xpord3ind  33416  wzel  33434  waj-ax  34249  lukshef-ax2  34250  bj-poni  34371  bj-currypeirce  34383  bj-axd2d  34421  bj-cbvalimt  34466  bj-eximcom  34470  bj-ssbeq  34480  bj-eqs  34502  bj-sbsb  34666  wl-axc11r  35335  finixpnum  35408  mbfresfi  35469  filbcmb  35544  orfa  35886  axc11n-16  36598  axc11-o  36611  axc5c4c711toc7  41583  axc5c4c711to11  41584  ax6e2nd  41739  elex22VD  42020  exbiriVD  42035  ssralv2VD  42047  truniALTVD  42059  trintALTVD  42061  onfrALTVD  42072  hbimpgVD  42085  ax6e2eqVD  42088  ax6e2ndVD  42089  2reu8i  44168  reupr  44538  reuopreuprim  44542  fmtnofac2lem  44584  sbgoldbwt  44793  sbgoldbst  44794  nnsum4primesodd  44812  nnsum4primesoddALTV  44813  bgoldbnnsum3prm  44820  tgoldbach  44833  snlindsntor  45376  itcovalt2  45587