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

Theorem pm2.27 39
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 31 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  pm2.43  51  com23  78  pm3.2im  145  mth8  146  biimt  335  pm3.35  587  a2andOLD  812  pm2.26  883  cases2  971  19.35  1687  axc112  1937  axc11n-16  2268  axc11-o  2281  issref  5385  tfinds  6694  tfindsg  6695  smogt  7057  findcard2  7780  findcard3  7783  fisupg  7788  xpfi  7811  dffi2  7903  cantnfle  8111  cantnfleOLD  8141  ac5num  8438  pwsdompw  8605  cfsmolem  8671  axcc4  8840  axdc3lem2  8852  fpwwe2lem8  9036  pwfseqlem3  9059  tskord  9179  grudomon  9216  grur1a  9218  xrub  11532  pcmptcl  14410  restntr  19683  cmpsublem  19899  cmpsub  19900  bwthOLD  19911  txlm  20149  ptcmplem3  20554  c1lip1  22398  wilthlem3  23344  dmdbr5  27227  wzel  29380  waj-ax  29879  lukshef-ax2  29880  finixpnum  30038  mbfresfi  30061  filbcmb  30231  orfa  30479  axc5c4c711toc7  31311  axc5c4c711to11  31312  snlindsntor  33072  ax6e2nd  33331  elex22VD  33639  exbiriVD  33654  ssralv2VD  33666  truniALTVD  33678  trintALTVD  33680  onfrALTVD  33691  hbimpgVD  33704  ax6e2eqVD  33707  ax6e2ndVD  33708  bj-axd2d  34181
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator