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  802  pm2.26  941  cases2ALT  1048  19.35  1876  19.36imv  1944  axc16g  2259  axc11r  2369  sb2  2482  mo4  2564  r19.35OLD  3096  r19.21v  3167  imadifssran  6151  reuop  6293  fundif  6595  tfinds  7863  tfindsg  7864  resf1extb  7938  xpord2indlem  8154  xpord3inddlem  8161  smogt  8389  findcard2  9186  findcard3  9300  findcard3OLD  9301  fisupg  9306  xpfiOLD  9341  dffi2  9445  fiinfg  9521  cantnfle  9693  ac5num  10058  pwsdompw  10225  cfsmolem  10292  axcc4  10461  axdc3lem2  10473  fpwwe2lem7  10659  pwfseqlem3  10682  tskord  10802  grudomon  10839  grur1a  10841  xrub  13336  relexprelg  15060  coprmproddvdslem  16682  pcmptcl  16912  restntr  23137  cmpsublem  23354  cmpsub  23355  txlm  23603  ptcmplem3  24009  c1lip1  25973  wilthlem3  27050  dmdbr5  32256  satfsschain  35344  satfrel  35347  satfdm  35349  satffun  35389  wzel  35800  waj-ax  36390  lukshef-ax2  36391  bj-poni  36521  bj-currypeirce  36533  bj-axd2d  36569  bj-cbvalimt  36615  bj-eximcom  36619  bj-ssbeq  36629  bj-eqs  36651  bj-sbsb  36813  wl-axc11r  37506  finixpnum  37587  mbfresfi  37648  filbcmb  37722  orfa  38064  axc11n-16  38914  axc11-o  38927  unielss  43208  axc5c4c711toc7  44395  axc5c4c711to11  44396  ax6e2nd  44550  elex22VD  44831  exbiriVD  44846  ssralv2VD  44858  truniALTVD  44870  trintALTVD  44872  onfrALTVD  44883  hbimpgVD  44896  ax6e2eqVD  44899  ax6e2ndVD  44900  2reu8i  47098  reupr  47482  reuopreuprim  47486  fmtnofac2lem  47528  sbgoldbwt  47737  sbgoldbst  47738  nnsum4primesodd  47756  nnsum4primesoddALTV  47757  bgoldbnnsum3prm  47764  tgoldbach  47777  snlindsntor  48361  itcovalt2  48571