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

Theorem mpani 676
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 11 . 2  |-  ( ph  ->  ps )
3 mpani.2 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
42, 3mpand 675 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mp2ani  678  ordelinel  4976  dif20el  7152  domunfican  7789  mulgt1  10397  recgt1i  10438  recreclt  10440  ledivp1i  10467  nngt0  10561  nnrecgt0  10569  elnnnn0c  10837  elnnz1  10886  recnz  10932  uz3m2nn  11120  xrub  11499  1mod  11992  expubnd  12190  expnbnd  12259  expnlbnd  12260  resqrex  13043  sin02gt0  13784  prmlem1  14447  prmlem2  14459  lsmss2  16482  ovolicopnf  21670  voliunlem3  21697  volsup  21701  volivth  21751  itg2seq  21884  itg2monolem2  21893  reeff1olem  22575  sinq12gt0  22633  logdivlti  22733  logdivlt  22734  efexple  23284  axlowdimlem16  23936  axlowdimlem17  23937  axlowdim  23940  dmdbr2  26898  dfon2lem3  28794  dfon2lem7  28798  wfi  28864  frind  28900  tan2h  29624  mblfinlem4  29631  nn0prpwlem  29717
  Copyright terms: Public domain W3C validator