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 40
Description: This theorem, called "Assertion," can be thought of as 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  53  com23  82  pm3.2im  152  mth8  153  biimt  344  pm3.35  603  pm2.26  913  cases2  995  19.35  1771  axc11r  2073  issref  5263  fundif  5678  tfinds  6763  tfindsg  6764  smogt  7163  findcard2  7896  findcard3  7899  fisupg  7904  xpfi  7927  dffi2  8022  fiinfg  8098  cantnfle  8261  ac5num  8552  pwsdompw  8719  cfsmolem  8785  axcc4  8954  axdc3lem2  8966  fpwwe2lem8  9147  pwfseqlem3  9170  tskord  9290  grudomon  9327  grur1a  9329  xrub  11692  relexprelg  13261  coprmproddvdslem  14841  pcmptcl  14998  restntr  20355  cmpsublem  20571  cmpsub  20572  txlm  20820  ptcmplem3  21227  c1lip1  23110  wilthlem3  24156  dmdbr5  28124  wzel  30658  waj-ax  31223  lukshef-ax2  31224  bj-axd2d  31360  bj-sbex  31421  bj-ssbeq  31422  bj-ssb0  31423  bj-eqs  31456  bj-sbsb  31621  finixpnum  32163  mbfresfi  32225  filbcmb  32305  orfa  32552  axc11n-16  32742  axc11-o  32755  axc5c4c711toc7  37112  axc5c4c711to11  37113  ax6e2nd  37281  elex22VD  37583  exbiriVD  37598  ssralv2VD  37611  truniALTVD  37623  trintALTVD  37625  onfrALTVD  37636  hbimpgVD  37649  ax6e2eqVD  37652  ax6e2ndVD  37653  bgoldbwt  39398  bgoldbst  39399  nnsum4primesodd  39411  nnsum4primesoddALTV  39412  bgoldbnnsum3prm  39419  tgoldbach  39431  snlindsntor  41454
  Copyright terms: Public domain W3C validator