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  1793  axc16g  2117  axc11rvOLD  2123  axc11r  2173  issref  5415  fundif  5835  tfinds  6928  tfindsg  6929  smogt  7328  findcard2  8062  findcard3  8065  fisupg  8070  xpfi  8093  dffi2  8189  fiinfg  8265  cantnfle  8428  ac5num  8719  pwsdompw  8886  cfsmolem  8952  axcc4  9121  axdc3lem2  9133  fpwwe2lem8  9315  pwfseqlem3  9338  tskord  9458  grudomon  9495  grur1a  9497  xrub  11970  relexprelg  13572  coprmproddvdslem  15160  pcmptcl  15379  restntr  20738  cmpsublem  20954  cmpsub  20955  txlm  21203  ptcmplem3  21610  c1lip1  23481  wilthlem3  24513  dmdbr5  28357  wzel  30821  wzelOLD  30822  waj-ax  31389  lukshef-ax2  31390  bj-axd2d  31556  bj-sbex  31621  bj-ssbeq  31622  bj-ssb0  31623  bj-eqs  31656  bj-sbsb  31825  finixpnum  32367  mbfresfi  32429  filbcmb  32508  orfa  32854  axc11n-16  33044  axc11-o  33057  axc5c4c711toc7  37430  axc5c4c711to11  37431  ax6e2nd  37598  elex22VD  37899  exbiriVD  37914  ssralv2VD  37927  truniALTVD  37939  trintALTVD  37941  onfrALTVD  37952  hbimpgVD  37965  ax6e2eqVD  37968  ax6e2ndVD  37969  fmtnofac2lem  39823  bgoldbwt  40004  bgoldbst  40005  nnsum4primesodd  40017  nnsum4primesoddALTV  40018  bgoldbnnsum3prm  40025  tgoldbach  40037  tgoldbachOLD  40044  snlindsntor  42056
  Copyright terms: Public domain W3C validator