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  4985  dif20el  7173  domunfican  7811  mulgt1  10422  recgt1i  10462  recreclt  10464  ledivp1i  10491  nngt0  10585  nnrecgt0  10594  elnnnn0c  10862  elnnz1  10911  recnz  10959  uz3m2nn  11148  xrub  11528  1mod  12031  expubnd  12229  expnbnd  12298  expnlbnd  12299  resqrex  13096  sin02gt0  13939  prmlem1  14605  prmlem2  14617  lsmss2  16813  ovolicopnf  22061  voliunlem3  22088  volsup  22092  volivth  22142  itg2seq  22275  itg2monolem2  22284  reeff1olem  22967  sinq12gt0  23026  logdivlti  23131  logdivlt  23132  efexple  23682  axlowdimlem16  24387  axlowdimlem17  24388  axlowdim  24391  dmdbr2  27349  dfon2lem3  29434  dfon2lem7  29438  wfi  29504  frind  29540  tan2h  30252  mblfinlem4  30259  nn0prpwlem  30345  pfx2  32530
  Copyright terms: Public domain W3C validator