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  4491  dif20el  6504  domunfican  7129  mulgt1  9615  recgt1i  9653  recreclt  9655  ledivp1i  9682  nngt0  9775  nnrecgt0  9783  elnnnn0c  10009  elnnz1  10049  recnz  10087  xrub  10630  1mod  10996  expubnd  11162  expnbnd  11230  expnlbnd  11231  resqrex  11736  sin02gt0  12472  prmlem1  13109  prmlem2  13121  lsmss2  14977  ovolicopnf  18883  voliunlem3  18909  volsup  18913  volivth  18962  itg2seq  19097  itg2monolem2  19106  reeff1olem  19822  sinq12gt0  19875  logdivlti  19971  logdivlt  19972  efexple  20520  dmdbr2  22883  dfon2lem3  24141  dfon2lem7  24145  wfi  24207  frind  24243  axlowdimlem16  24585  axlowdimlem17  24586  axlowdim  24589  tareltsuc  25898  nn0prpwlem  26238
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