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

Theorem mpani 658
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 657 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mp2ani  660  ordelinel  4639  dif20el  6708  domunfican  7338  mulgt1  9825  recgt1i  9863  recreclt  9865  ledivp1i  9892  nngt0  9985  nnrecgt0  9993  elnnnn0c  10221  elnnz1  10263  recnz  10301  xrub  10846  1mod  11228  expubnd  11395  expnbnd  11463  expnlbnd  11464  resqrex  12011  sin02gt0  12748  prmlem1  13385  prmlem2  13397  lsmss2  15255  ovolicopnf  19373  voliunlem3  19399  volsup  19403  volivth  19452  itg2seq  19587  itg2monolem2  19596  reeff1olem  20315  sinq12gt0  20368  logdivlti  20468  logdivlt  20469  efexple  21018  dmdbr2  23759  dfon2lem3  25355  dfon2lem7  25359  wfi  25421  frind  25457  axlowdimlem16  25800  axlowdimlem17  25801  axlowdim  25804  mblfinlem3  26145  nn0prpwlem  26215
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 178  df-an 361
  Copyright terms: Public domain W3C validator