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  163  jcn  165  biimt  364  pm3.35  802  pm2.26  937  cases2ALT  1044  19.35  1879  spsbeOLD  2090  axc16g  2262  axc11r  2387  sb2  2505  mo4  2650  r19.35  3326  reuop  6117  fundif  6376  tfinds  7549  tfindsg  7550  smogt  7979  findcard2  8734  findcard3  8737  fisupg  8742  xpfi  8765  dffi2  8863  fiinfg  8939  cantnfle  9110  ac5num  9439  pwsdompw  9603  cfsmolem  9669  axcc4  9838  axdc3lem2  9850  fpwwe2lem8  10036  pwfseqlem3  10059  tskord  10179  grudomon  10216  grur1a  10218  xrub  12683  relexprelg  14376  coprmproddvdslem  15983  pcmptcl  16204  restntr  21765  cmpsublem  21982  cmpsub  21983  txlm  22231  ptcmplem3  22637  c1lip1  24578  wilthlem3  25633  dmdbr5  30069  satfsschain  32618  satfrel  32621  satfdm  32623  satffun  32663  wzel  33118  waj-ax  33769  lukshef-ax2  33770  bj-currypeirce  33899  bj-axd2d  33934  bj-cbvalimt  33979  bj-eximcom  33983  bj-ssbeq  33993  bj-eqs  34015  bj-sbsb  34167  wl-axc11r  34813  finixpnum  34920  mbfresfi  34981  filbcmb  35056  orfa  35398  axc11n-16  36112  axc11-o  36125  axc5c4c711toc7  40891  axc5c4c711to11  40892  ax6e2nd  41047  elex22VD  41328  exbiriVD  41343  ssralv2VD  41355  truniALTVD  41367  trintALTVD  41369  onfrALTVD  41380  hbimpgVD  41393  ax6e2eqVD  41396  ax6e2ndVD  41397  2reu8i  43460  reupr  43830  reuopreuprim  43834  fmtnofac2lem  43876  sbgoldbwt  44087  sbgoldbst  44088  nnsum4primesodd  44106  nnsum4primesoddALTV  44107  bgoldbnnsum3prm  44114  tgoldbach  44127  snlindsntor  44671  itcovalt2  44851
  Copyright terms: Public domain W3C validator