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 41
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  54  com23  84  pm3.2im  156  mth8  157  biimt  349  pm3.35  609  pm2.26  923  cases2  1005  19.35  1794  axc16g  2119  axc11rvOLD  2125  axc11r  2175  issref  5428  fundif  5849  tfinds  6951  tfindsg  6952  smogt  7351  findcard2  8085  findcard3  8088  fisupg  8093  xpfi  8116  dffi2  8212  fiinfg  8288  cantnfle  8451  ac5num  8742  pwsdompw  8909  cfsmolem  8975  axcc4  9144  axdc3lem2  9156  fpwwe2lem8  9338  pwfseqlem3  9361  tskord  9481  grudomon  9518  grur1a  9520  xrub  12014  relexprelg  13626  coprmproddvdslem  15214  pcmptcl  15433  restntr  20796  cmpsublem  21012  cmpsub  21013  txlm  21261  ptcmplem3  21668  c1lip1  23564  wilthlem3  24596  dmdbr5  28551  wzel  31015  wzelOLD  31016  waj-ax  31583  lukshef-ax2  31584  bj-axd2d  31750  bj-sbex  31815  bj-ssbeq  31816  bj-ssb0  31817  bj-eqs  31850  bj-sbsb  32012  finixpnum  32564  mbfresfi  32626  filbcmb  32705  orfa  33051  axc11n-16  33241  axc11-o  33254  axc5c4c711toc7  37627  axc5c4c711to11  37628  ax6e2nd  37795  elex22VD  38096  exbiriVD  38111  ssralv2VD  38124  truniALTVD  38136  trintALTVD  38138  onfrALTVD  38149  hbimpgVD  38162  ax6e2eqVD  38165  ax6e2ndVD  38166  fmtnofac2lem  40018  bgoldbwt  40199  bgoldbst  40200  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  bgoldbnnsum3prm  40220  tgoldbach  40232  tgoldbachOLD  40239  snlindsntor  42054
  Copyright terms: Public domain W3C validator