Theorem pm2.27 43

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 23	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓))
2	1	com12 33	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  57  com23  87  pm3.2im  161  jcn  163  biimt  363  pm3.35  814  pm2.26  954  cases2ALT  1064  19.35  1907  19.36imv  1975  axc16g  2296  axc11r  2400  sb2  2511  mo4  2594  r19.21v  3190  replem  5250  imadifssran  6204  imadifssranOLD  6205  reuop  6296  fundif  6587  tfinds  7857  tfindsg  7858  resf1extb  7932  xpord2indlem  8144  xpord3inddlem  8151  smogt  8355  findcard2  9150  findcard3  9244  fisupg  9249  dffi2  9384  fiinfg  9462  cantnfle  9641  ac5num  10021  pwsdompw  10187  cfsmolem  10255  axcc4  10424  axdc3lem2  10436  fpwwe2lem7  10623  pwfseqlem3  10646  tskord  10766  grudomon  10803  grur1a  10805  xrub  13339  relexprelg  15077  coprmproddvdslem  16721  pcmptcl  16952  restntr  23320  cmpsublem  23537  cmpsub  23538  txlm  23786  ptcmplem3  24192  c1lip1  26137  wilthlem3  27212  oldfib  28548  dmdbr5  32638  satfsschain  35834  satfrel  35837  satfdm  35839  satffun  35879  antnestlaw1  36161  antnestlaw2  36162  antnestALT  36164  wzel  36292  waj-ax  36903  lukshef-ax2  36904  bj-poni  37111  bj-currypeirce  37127  bj-axd2d  37164  bj-eximcom  37217  bj-alextruim  37237  bj-ssbeq  37253  bj-eqs  37276  bj-sbsb  37450  wl-axc11r  38163  finixpnum  38234  mbfresfi  38295  filbcmb  38369  orfa  38711  axc11n-16  39690  axc11-o  39703  unielss  43925  axc5c4c711toc7  45094  axc5c4c711to11  45095  ax6e2nd  45247  elex22VD  45527  exbiriVD  45542  ssralv2VD  45554  truniALTVD  45566  trintALTVD  45568  onfrALTVD  45579  hbimpgVD  45592  ax6e2eqVD  45595  ax6e2ndVD  45596  2reu8i  47827  reupr  48248  reuopreuprim  48252  fmtnofac2lem  48297  sbgoldbwt  48519  sbgoldbst  48520  nnsum4primesodd  48538  nnsum4primesoddALTV  48539  bgoldbnnsum3prm  48546  tgoldbach  48559  gpgprismgr4cycllem2  48838  snlindsntor  49228  itcovalt2  49434