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  349  pm3.35  612  pm2.26  963  cases2ALT  1035  19.35  1946  axc16g  2273  axc11rvOLD  2279  axc11r  2324  issref  5659  fundif  6088  tfinds  7216  tfindsg  7217  smogt  7625  findcard2  8357  findcard3  8360  fisupg  8365  xpfi  8388  dffi2  8486  fiinfg  8562  cantnfle  8733  ac5num  9041  pwsdompw  9210  cfsmolem  9276  axcc4  9445  axdc3lem2  9457  fpwwe2lem8  9643  pwfseqlem3  9666  tskord  9786  grudomon  9823  grur1a  9825  xrub  12327  relexprelg  13969  coprmproddvdslem  15570  pcmptcl  15789  restntr  21180  cmpsublem  21396  cmpsub  21397  txlm  21645  ptcmplem3  22051  c1lip1  23951  wilthlem3  24987  dmdbr5  29468  wzel  32067  waj-ax  32711  lukshef-ax2  32712  bj-axd2d  32875  bj-sbex  32924  bj-ssbeq  32925  bj-ssb0  32926  bj-eqs  32961  bj-sbsb  33122  finixpnum  33699  mbfresfi  33761  filbcmb  33840  orfa  34186  axc11n-16  34719  axc11-o  34732  axc5c4c711toc7  39099  axc5c4c711to11  39100  ax6e2nd  39268  elex22VD  39565  exbiriVD  39580  ssralv2VD  39593  truniALTVD  39605  trintALTVD  39607  onfrALTVD  39618  hbimpgVD  39631  ax6e2eqVD  39634  ax6e2ndVD  39635  fmtnofac2lem  41982  sbgoldbwt  42167  sbgoldbst  42168  nnsum4primesodd  42186  nnsum4primesoddALTV  42187  bgoldbnnsum3prm  42194  tgoldbach  42207  tgoldbachOLD  42214  snlindsntor  42762
  Copyright terms: Public domain W3C validator