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  4924  dif20el  7054  domunfican  7694  mulgt1  10298  recgt1i  10339  recreclt  10341  ledivp1i  10368  nngt0  10461  nnrecgt0  10469  elnnnn0c  10735  elnnz1  10782  recnz  10827  xrub  11384  1mod  11856  expubnd  12040  expnbnd  12109  expnlbnd  12110  resqrex  12857  sin02gt0  13593  prmlem1  14252  prmlem2  14264  lsmss2  16285  ovolicopnf  21138  voliunlem3  21165  volsup  21169  volivth  21219  itg2seq  21352  itg2monolem2  21361  reeff1olem  22043  sinq12gt0  22101  logdivlti  22201  logdivlt  22202  efexple  22752  axlowdimlem16  23354  axlowdimlem17  23355  axlowdim  23358  dmdbr2  25858  dfon2lem3  27741  dfon2lem7  27745  wfi  27811  frind  27847  tan2h  28571  mblfinlem4  28578  nn0prpwlem  28664  uz3m2nn  30342
  Copyright terms: Public domain W3C validator