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  159  mth8  160  biimt  352  pm3.35  839  pm2.26  970  cases2ALT  1077  19.35  1982  axc16g  2292  axc11r  2390  idrefOLD  5751  fundif  6171  tfinds  7320  tfindsg  7321  smogt  7730  findcard2  8469  findcard3  8472  fisupg  8477  xpfi  8500  dffi2  8598  fiinfg  8674  cantnfle  8845  ac5num  9172  pwsdompw  9341  cfsmolem  9407  axcc4  9576  axdc3lem2  9588  fpwwe2lem8  9774  pwfseqlem3  9797  tskord  9917  grudomon  9954  grur1a  9956  xrub  12430  relexprelg  14155  coprmproddvdslem  15748  pcmptcl  15966  restntr  21357  cmpsublem  21573  cmpsub  21574  txlm  21822  ptcmplem3  22228  c1lip1  24159  wilthlem3  25209  dmdbr5  29722  wzel  32308  waj-ax  32946  lukshef-ax2  32947  bj-axd2d  33106  bj-cbvalimt  33148  bj-sbex  33163  bj-ssbeq  33164  bj-ssb0  33165  bj-eqs  33198  bj-sbsb  33348  finixpnum  33937  mbfresfi  33999  filbcmb  34078  orfa  34423  axc11n-16  35013  axc11-o  35026  axc5c4c711toc7  39444  axc5c4c711to11  39445  ax6e2nd  39602  elex22VD  39893  exbiriVD  39908  ssralv2VD  39920  truniALTVD  39932  trintALTVD  39934  onfrALTVD  39945  hbimpgVD  39958  ax6e2eqVD  39961  ax6e2ndVD  39962  fmtnofac2lem  42310  sbgoldbwt  42495  sbgoldbst  42496  nnsum4primesodd  42514  nnsum4primesoddALTV  42515  bgoldbnnsum3prm  42522  tgoldbach  42535  snlindsntor  43107