Theorem pm2.27 42

Description: This theorem, called "Assertion," can be thought of as 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  157  mth8  158  biimt  350  pm3.35  611  pm2.26  927  cases2  993  19.35  1805  axc16g  2134  axc11rvOLD  2140  axc11r  2187  issref  5509  fundif  5935  tfinds  7059  tfindsg  7060  smogt  7464  findcard2  8200  findcard3  8203  fisupg  8208  xpfi  8231  dffi2  8329  fiinfg  8405  cantnfle  8568  ac5num  8859  pwsdompw  9026  cfsmolem  9092  axcc4  9261  axdc3lem2  9273  fpwwe2lem8  9459  pwfseqlem3  9482  tskord  9602  grudomon  9639  grur1a  9641  xrub  12142  relexprelg  13778  coprmproddvdslem  15376  pcmptcl  15595  restntr  20986  cmpsublem  21202  cmpsub  21203  txlm  21451  ptcmplem3  21858  c1lip1  23760  wilthlem3  24796  dmdbr5  29167  wzel  31771  wzelOLD  31772  waj-ax  32413  lukshef-ax2  32414  bj-axd2d  32577  bj-sbex  32626  bj-ssbeq  32627  bj-ssb0  32628  bj-eqs  32663  bj-sbsb  32824  finixpnum  33394  mbfresfi  33456  filbcmb  33535  orfa  33881  axc11n-16  34223  axc11-o  34236  axc5c4c711toc7  38605  axc5c4c711to11  38606  ax6e2nd  38774  elex22VD  39074  exbiriVD  39089  ssralv2VD  39102  truniALTVD  39114  trintALTVD  39116  onfrALTVD  39127  hbimpgVD  39140  ax6e2eqVD  39143  ax6e2ndVD  39144  fmtnofac2lem  41480  sbgoldbwt  41665  sbgoldbst  41666  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  bgoldbnnsum3prm  41692  tgoldbach  41705  tgoldbachOLD  41712  snlindsntor  42260