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  803  pm2.26  942  cases2ALT  1049  19.35  1879  19.36imv  1947  axc16g  2268  axc11r  2372  sb2  2483  mo4  2566  r19.21v  3162  replem  5223  imadifssran  6115  reuop  6257  fundif  6547  tfinds  7811  tfindsg  7812  resf1extb  7885  xpord2indlem  8097  xpord3inddlem  8104  smogt  8307  findcard2  9099  findcard3  9193  fisupg  9198  dffi2  9336  fiinfg  9414  cantnfle  9592  ac5num  9958  pwsdompw  10125  cfsmolem  10192  axcc4  10361  axdc3lem2  10373  fpwwe2lem7  10560  pwfseqlem3  10583  tskord  10703  grudomon  10740  grur1a  10742  xrub  13264  relexprelg  15000  coprmproddvdslem  16631  pcmptcl  16862  restntr  23147  cmpsublem  23364  cmpsub  23365  txlm  23613  ptcmplem3  24019  c1lip1  25964  wilthlem3  27033  oldfib  28369  dmdbr5  32379  satfsschain  35546  satfrel  35549  satfdm  35551  satffun  35591  antnestlaw1  35873  antnestlaw2  35874  antnestALT  35876  wzel  36004  waj-ax  36596  lukshef-ax2  36597  bj-poni  36805  bj-currypeirce  36821  bj-axd2d  36858  bj-eximcom  36911  bj-alextruim  36931  bj-ssbeq  36947  bj-eqs  36970  bj-sbsb  37144  wl-axc11r  37855  finixpnum  37926  mbfresfi  37987  filbcmb  38061  orfa  38403  axc11n-16  39384  axc11-o  39397  unielss  43646  axc5c4c711toc7  44831  axc5c4c711to11  44832  ax6e2nd  44985  elex22VD  45265  exbiriVD  45280  ssralv2VD  45292  truniALTVD  45304  trintALTVD  45306  onfrALTVD  45317  hbimpgVD  45330  ax6e2eqVD  45333  ax6e2ndVD  45334  2reu8i  47561  reupr  47982  reuopreuprim  47986  fmtnofac2lem  48031  sbgoldbwt  48253  sbgoldbst  48254  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  bgoldbnnsum3prm  48280  tgoldbach  48293  gpgprismgr4cycllem2  48572  snlindsntor  48947  itcovalt2  49153