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  158  mth8  159  biimt  349  pm3.35  798  pm2.26  919  cases2ALT  1033  19.35  1957  axc16g  2299  axc11rvOLD  2305  axc11r  2349  issref  5651  fundif  6079  tfinds  7207  tfindsg  7208  smogt  7618  findcard2  8357  findcard3  8360  fisupg  8365  xpfi  8388  dffi2  8486  fiinfg  8562  cantnfle  8733  ac5num  9060  pwsdompw  9229  cfsmolem  9295  axcc4  9464  axdc3lem2  9476  fpwwe2lem8  9662  pwfseqlem3  9685  tskord  9805  grudomon  9842  grur1a  9844  xrub  12348  relexprelg  13987  coprmproddvdslem  15584  pcmptcl  15803  restntr  21208  cmpsublem  21424  cmpsub  21425  txlm  21673  ptcmplem3  22079  c1lip1  23981  wilthlem3  25018  dmdbr5  29508  wzel  32107  waj-ax  32751  lukshef-ax2  32752  bj-axd2d  32915  bj-sbex  32965  bj-ssbeq  32966  bj-ssb0  32967  bj-eqs  33001  bj-sbsb  33160  finixpnum  33728  mbfresfi  33789  filbcmb  33868  orfa  34214  axc11n-16  34747  axc11-o  34760  axc5c4c711toc7  39132  axc5c4c711to11  39133  ax6e2nd  39300  elex22VD  39597  exbiriVD  39612  ssralv2VD  39625  truniALTVD  39637  trintALTVD  39639  onfrALTVD  39650  hbimpgVD  39663  ax6e2eqVD  39666  ax6e2ndVD  39667  fmtnofac2lem  42009  sbgoldbwt  42194  sbgoldbst  42195  nnsum4primesodd  42213  nnsum4primesoddALTV  42214  bgoldbnnsum3prm  42221  tgoldbach  42234  tgoldbachOLD  42241  snlindsntor  42789
  Copyright terms: Public domain W3C validator