MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.27 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 id 22 . 2 ((𝜑𝜓) → (𝜑𝜓))
21com12 32 1 (𝜑 → ((𝜑𝜓) → 𝜓))
Colors of variables: wff setvar class
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  162  mth8  163  biimt  362  pm3.35  799  pm2.26  933  cases2ALT  1040  19.35  1869  spsbeOLD  2080  axc16g  2251  axc11r  2377  sb2  2497  mo4  2643  r19.35  3338  reuop  6137  fundif  6396  tfinds  7563  tfindsg  7564  smogt  7993  findcard2  8746  findcard3  8749  fisupg  8754  xpfi  8777  dffi2  8875  fiinfg  8951  cantnfle  9122  ac5num  9450  pwsdompw  9614  cfsmolem  9680  axcc4  9849  axdc3lem2  9861  fpwwe2lem8  10047  pwfseqlem3  10070  tskord  10190  grudomon  10227  grur1a  10229  xrub  12693  relexprelg  14385  coprmproddvdslem  15994  pcmptcl  16215  restntr  21718  cmpsublem  21935  cmpsub  21936  txlm  22184  ptcmplem3  22590  c1lip1  24521  wilthlem3  25574  dmdbr5  30012  satfsschain  32508  satfrel  32511  satfdm  32513  satffun  32553  wzel  33008  waj-ax  33659  lukshef-ax2  33660  bj-currypeirce  33789  bj-axd2d  33824  bj-cbvalimt  33869  bj-eximcom  33873  bj-ssbeq  33883  bj-eqs  33905  bj-sbsb  34057  finixpnum  34758  mbfresfi  34819  filbcmb  34896  orfa  35241  axc11n-16  35954  axc11-o  35967  axc5c4c711toc7  40613  axc5c4c711to11  40614  ax6e2nd  40769  elex22VD  41050  exbiriVD  41065  ssralv2VD  41077  truniALTVD  41089  trintALTVD  41091  onfrALTVD  41102  hbimpgVD  41115  ax6e2eqVD  41118  ax6e2ndVD  41119  2reu8i  43189  reupr  43561  reuopreuprim  43565  fmtnofac2lem  43607  sbgoldbwt  43819  sbgoldbst  43820  nnsum4primesodd  43838  nnsum4primesoddALTV  43839  bgoldbnnsum3prm  43846  tgoldbach  43859  snlindsntor  44454
  Copyright terms: Public domain W3C validator