MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpani Structured version   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  4672  dif20el  6741  domunfican  7371  mulgt1  9861  recgt1i  9899  recreclt  9901  ledivp1i  9928  nngt0  10021  nnrecgt0  10029  elnnnn0c  10257  elnnz1  10299  recnz  10337  xrub  10882  1mod  11265  expubnd  11432  expnbnd  11500  expnlbnd  11501  resqrex  12048  sin02gt0  12785  prmlem1  13422  prmlem2  13434  lsmss2  15292  ovolicopnf  19412  voliunlem3  19438  volsup  19442  volivth  19491  itg2seq  19626  itg2monolem2  19635  reeff1olem  20354  sinq12gt0  20407  logdivlti  20507  logdivlt  20508  efexple  21057  dmdbr2  23798  dfon2lem3  25404  dfon2lem7  25408  wfi  25474  frind  25510  axlowdimlem16  25888  axlowdimlem17  25889  axlowdim  25892  mblfinlem3  26236  nn0prpwlem  26316
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