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 42
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  56  com23  86  pm3.2im  157  mth8  158  biimt  350  pm3.35  610  pm2.26  926  cases2  992  19.35  1802  axc16g  2130  axc11rvOLD  2136  axc11r  2186  issref  5468  fundif  5893  tfinds  7006  tfindsg  7007  smogt  7409  findcard2  8144  findcard3  8147  fisupg  8152  xpfi  8175  dffi2  8273  fiinfg  8349  cantnfle  8512  ac5num  8803  pwsdompw  8970  cfsmolem  9036  axcc4  9205  axdc3lem2  9217  fpwwe2lem8  9403  pwfseqlem3  9426  tskord  9546  grudomon  9583  grur1a  9585  xrub  12085  relexprelg  13712  coprmproddvdslem  15300  pcmptcl  15519  restntr  20896  cmpsublem  21112  cmpsub  21113  txlm  21361  ptcmplem3  21768  c1lip1  23664  wilthlem3  24696  dmdbr5  29016  wzel  31472  wzelOLD  31473  waj-ax  32055  lukshef-ax2  32056  bj-axd2d  32219  bj-sbex  32268  bj-ssbeq  32269  bj-ssb0  32270  bj-eqs  32305  bj-sbsb  32467  finixpnum  33026  mbfresfi  33088  filbcmb  33167  orfa  33513  axc11n-16  33703  axc11-o  33716  axc5c4c711toc7  38087  axc5c4c711to11  38088  ax6e2nd  38256  elex22VD  38557  exbiriVD  38572  ssralv2VD  38585  truniALTVD  38597  trintALTVD  38599  onfrALTVD  38610  hbimpgVD  38623  ax6e2eqVD  38626  ax6e2ndVD  38627  fmtnofac2lem  40779  bgoldbwt  40960  bgoldbst  40961  nnsum4primesodd  40973  nnsum4primesoddALTV  40974  bgoldbnnsum3prm  40981  tgoldbach  40993  tgoldbachOLD  41000  snlindsntor  41548
  Copyright terms: Public domain W3C validator