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  1062  19.35  1900  19.36imv  1968  axc16g  2298  axc11r  2402  sb2  2513  mo4  2596  r19.21v  3190  replem  5243  imadifssran  6140  reuop  6284  fundif  6574  tfinds  7844  tfindsg  7845  resf1extb  7919  xpord2indlem  8131  xpord3inddlem  8138  smogt  8342  findcard2  9137  findcard3  9231  fisupg  9236  dffi2  9371  fiinfg  9449  cantnfle  9628  ac5num  10008  pwsdompw  10174  cfsmolem  10242  axcc4  10411  axdc3lem2  10423  fpwwe2lem7  10610  pwfseqlem3  10633  tskord  10753  grudomon  10790  grur1a  10792  xrub  13329  relexprelg  15065  coprmproddvdslem  16710  pcmptcl  16941  restntr  23300  cmpsublem  23517  cmpsub  23518  txlm  23766  ptcmplem3  24172  c1lip1  26117  wilthlem3  27192  oldfib  28528  dmdbr5  32569  satfsschain  35727  satfrel  35730  satfdm  35732  satffun  35772  antnestlaw1  36054  antnestlaw2  36055  antnestALT  36057  wzel  36185  waj-ax  36787  lukshef-ax2  36788  bj-poni  36995  bj-currypeirce  37011  bj-axd2d  37048  bj-eximcom  37101  bj-alextruim  37121  bj-ssbeq  37137  bj-eqs  37160  bj-sbsb  37334  wl-axc11r  38045  finixpnum  38116  mbfresfi  38177  filbcmb  38251  orfa  38593  axc11n-16  39574  axc11-o  39587  unielss  43807  axc5c4c711toc7  44978  axc5c4c711to11  44979  ax6e2nd  45132  elex22VD  45412  exbiriVD  45427  ssralv2VD  45439  truniALTVD  45451  trintALTVD  45453  onfrALTVD  45464  hbimpgVD  45477  ax6e2eqVD  45480  ax6e2ndVD  45481  2reu8i  47705  reupr  48126  reuopreuprim  48130  fmtnofac2lem  48175  sbgoldbwt  48397  sbgoldbst  48398  nnsum4primesodd  48416  nnsum4primesoddALTV  48417  bgoldbnnsum3prm  48424  tgoldbach  48437  gpgprismgr4cycllem2  48716  snlindsntor  49102  itcovalt2  49308