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  359  pm3.35  799  pm2.26  936  cases2ALT  1045  19.35  1878  19.36imv  1946  axc16g  2249  axc11r  2363  sb2  2476  mo4  2558  r19.35OLD  3107  r19.21v  3177  ab0OLD  4376  reuop  6293  fundif  6598  tfinds  7853  tfindsg  7854  xpord2indlem  8137  xpord3inddlem  8144  smogt  8371  findcard2  9168  findcard2OLD  9288  findcard3  9289  findcard3OLD  9290  fisupg  9295  xpfiOLD  9322  dffi2  9422  fiinfg  9498  cantnfle  9670  ac5num  10035  pwsdompw  10203  cfsmolem  10269  axcc4  10438  axdc3lem2  10450  fpwwe2lem7  10636  pwfseqlem3  10659  tskord  10779  grudomon  10816  grur1a  10818  xrub  13297  relexprelg  14991  coprmproddvdslem  16605  pcmptcl  16830  restntr  22908  cmpsublem  23125  cmpsub  23126  txlm  23374  ptcmplem3  23780  c1lip1  25748  wilthlem3  26808  dmdbr5  31826  satfsschain  34651  satfrel  34654  satfdm  34656  satffun  34696  wzel  35098  waj-ax  35604  lukshef-ax2  35605  bj-poni  35726  bj-currypeirce  35738  bj-axd2d  35776  bj-cbvalimt  35821  bj-eximcom  35825  bj-ssbeq  35835  bj-eqs  35857  bj-sbsb  36020  wl-axc11r  36704  finixpnum  36778  mbfresfi  36839  filbcmb  36913  orfa  37255  axc11n-16  38113  axc11-o  38126  unielss  42271  axc5c4c711toc7  43467  axc5c4c711to11  43468  ax6e2nd  43623  elex22VD  43904  exbiriVD  43919  ssralv2VD  43931  truniALTVD  43943  trintALTVD  43945  onfrALTVD  43956  hbimpgVD  43969  ax6e2eqVD  43972  ax6e2ndVD  43973  2reu8i  46121  reupr  46490  reuopreuprim  46494  fmtnofac2lem  46536  sbgoldbwt  46745  sbgoldbst  46746  nnsum4primesodd  46764  nnsum4primesoddALTV  46765  bgoldbnnsum3prm  46772  tgoldbach  46785  snlindsntor  47241  itcovalt2  47452