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  360  pm3.35  800  pm2.26  937  cases2ALT  1046  19.35  1879  19.36imv  1947  axc16g  2250  axc11r  2364  sb2  2477  mo4  2559  r19.35OLD  3108  r19.21v  3178  ab0OLD  4375  reuop  6292  fundif  6597  tfinds  7853  tfindsg  7854  xpord2indlem  8138  xpord3inddlem  8145  smogt  8373  findcard2  9170  findcard2OLD  9290  findcard3  9291  findcard3OLD  9292  fisupg  9297  xpfiOLD  9324  dffi2  9424  fiinfg  9500  cantnfle  9672  ac5num  10037  pwsdompw  10205  cfsmolem  10271  axcc4  10440  axdc3lem2  10452  fpwwe2lem7  10638  pwfseqlem3  10661  tskord  10781  grudomon  10818  grur1a  10820  xrub  13298  relexprelg  14992  coprmproddvdslem  16606  pcmptcl  16831  restntr  22919  cmpsublem  23136  cmpsub  23137  txlm  23385  ptcmplem3  23791  c1lip1  25763  wilthlem3  26825  dmdbr5  31843  satfsschain  34668  satfrel  34671  satfdm  34673  satffun  34713  wzel  35115  waj-ax  35615  lukshef-ax2  35616  bj-poni  35737  bj-currypeirce  35749  bj-axd2d  35787  bj-cbvalimt  35832  bj-eximcom  35836  bj-ssbeq  35846  bj-eqs  35868  bj-sbsb  36031  wl-axc11r  36715  finixpnum  36789  mbfresfi  36850  filbcmb  36924  orfa  37266  axc11n-16  38124  axc11-o  38137  unielss  42282  axc5c4c711toc7  43478  axc5c4c711to11  43479  ax6e2nd  43634  elex22VD  43915  exbiriVD  43930  ssralv2VD  43942  truniALTVD  43954  trintALTVD  43956  onfrALTVD  43967  hbimpgVD  43980  ax6e2eqVD  43983  ax6e2ndVD  43984  2reu8i  46132  reupr  46501  reuopreuprim  46505  fmtnofac2lem  46547  sbgoldbwt  46756  sbgoldbst  46757  nnsum4primesodd  46775  nnsum4primesoddALTV  46776  bgoldbnnsum3prm  46783  tgoldbach  46796  snlindsntor  47252  itcovalt2  47463