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  83  pm3.2im  155  mth8  156  biimt  348  pm3.35  608  pm2.26  922  cases2  1004  19.35  1775  axc11rv  2068  axc11r  2136  issref  5319  fundif  5734  tfinds  6826  tfindsg  6827  smogt  7226  findcard2  7960  findcard3  7963  fisupg  7968  xpfi  7991  dffi2  8087  fiinfg  8163  cantnfle  8326  ac5num  8617  pwsdompw  8784  cfsmolem  8850  axcc4  9019  axdc3lem2  9031  fpwwe2lem8  9213  pwfseqlem3  9236  tskord  9356  grudomon  9393  grur1a  9395  xrub  11879  relexprelg  13483  coprmproddvdslem  15088  pcmptcl  15315  restntr  20697  cmpsublem  20913  cmpsub  20914  txlm  21162  ptcmplem3  21569  c1lip1  23440  wilthlem3  24484  dmdbr5  28340  wzel  30853  waj-ax  31418  lukshef-ax2  31419  bj-axd2d  31585  bj-sbex  31650  bj-ssbeq  31651  bj-ssb0  31652  bj-eqs  31685  bj-sbsb  31854  finixpnum  32439  mbfresfi  32501  filbcmb  32580  orfa  32926  axc11n-16  33116  axc11-o  33129  axc5c4c711toc7  37509  axc5c4c711to11  37510  ax6e2nd  37677  elex22VD  37978  exbiriVD  37993  ssralv2VD  38006  truniALTVD  38018  trintALTVD  38020  onfrALTVD  38031  hbimpgVD  38044  ax6e2eqVD  38047  ax6e2ndVD  38048  fmtnofac2lem  39913  bgoldbwt  40094  bgoldbst  40095  nnsum4primesodd  40107  nnsum4primesoddALTV  40108  bgoldbnnsum3prm  40115  tgoldbach  40127  tgoldbachOLD  40134  snlindsntor  42146
  Copyright terms: Public domain W3C validator