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  361  pm3.35  808  pm2.26  947  cases2ALT  1054  19.35  1884  19.36imv  1952  axc16g  2272  axc11r  2376  sb2  2487  mo4  2570  r19.21v  3165  replem  5217  imadifssran  6109  reuop  6251  fundif  6541  tfinds  7807  tfindsg  7808  resf1extb  7881  xpord2indlem  8094  xpord3inddlem  8101  smogt  8304  findcard2  9096  findcard3  9190  fisupg  9195  dffi2  9333  fiinfg  9411  cantnfle  9590  ac5num  9956  pwsdompw  10123  cfsmolem  10190  axcc4  10359  axdc3lem2  10371  fpwwe2lem7  10558  pwfseqlem3  10581  tskord  10701  grudomon  10738  grur1a  10740  xrub  13262  relexprelg  14998  coprmproddvdslem  16629  pcmptcl  16860  restntr  23172  cmpsublem  23389  cmpsub  23390  txlm  23638  ptcmplem3  24044  c1lip1  25989  wilthlem3  27058  oldfib  28394  dmdbr5  32404  satfsschain  35599  satfrel  35602  satfdm  35604  satffun  35644  antnestlaw1  35926  antnestlaw2  35927  antnestALT  35929  wzel  36057  waj-ax  36649  lukshef-ax2  36650  bj-poni  36858  bj-currypeirce  36874  bj-axd2d  36911  bj-eximcom  36964  bj-alextruim  36984  bj-ssbeq  37000  bj-eqs  37023  bj-sbsb  37197  wl-axc11r  37908  finixpnum  37979  mbfresfi  38040  filbcmb  38114  orfa  38456  axc11n-16  39437  axc11-o  39450  unielss  43670  axc5c4c711toc7  44855  axc5c4c711to11  44856  ax6e2nd  45009  elex22VD  45289  exbiriVD  45304  ssralv2VD  45316  truniALTVD  45328  trintALTVD  45330  onfrALTVD  45341  hbimpgVD  45354  ax6e2eqVD  45357  ax6e2ndVD  45358  2reu8i  47583  reupr  48004  reuopreuprim  48008  fmtnofac2lem  48053  sbgoldbwt  48275  sbgoldbst  48276  nnsum4primesodd  48294  nnsum4primesoddALTV  48295  bgoldbnnsum3prm  48302  tgoldbach  48315  gpgprismgr4cycllem2  48594  snlindsntor  48969  itcovalt2  49175