MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpani Unicode version

Theorem mpani 657
Description: An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
Hypotheses
Ref Expression
mpani.1  |-  ps
mpani.2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
mpani  |-  ( ph  ->  ( ch  ->  th )
)

Proof of Theorem mpani
StepHypRef Expression
1 mpani.1 . . 3  |-  ps
21a1i 10 . 2  |-  ( ph  ->  ps )
3 mpani.2 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
42, 3mpand 656 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mp2ani  659  ordelinel  4507  dif20el  6520  domunfican  7145  mulgt1  9631  recgt1i  9669  recreclt  9671  ledivp1i  9698  nngt0  9791  nnrecgt0  9799  elnnnn0c  10025  elnnz1  10065  recnz  10103  xrub  10646  1mod  11012  expubnd  11178  expnbnd  11246  expnlbnd  11247  resqrex  11752  sin02gt0  12488  prmlem1  13125  prmlem2  13137  lsmss2  14993  ovolicopnf  18899  voliunlem3  18925  volsup  18929  volivth  18978  itg2seq  19113  itg2monolem2  19122  reeff1olem  19838  sinq12gt0  19891  logdivlti  19987  logdivlt  19988  efexple  20536  dmdbr2  22899  dfon2lem3  24212  dfon2lem7  24216  wfi  24278  frind  24314  axlowdimlem16  24657  axlowdimlem17  24658  axlowdim  24661  tareltsuc  26001  nn0prpwlem  26341
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator