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

Theorem mpani 687
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 686 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  mp2ani  689  wfi  5392  ordelinel  5500  dif20el  7194  domunfican  7831  mulgt1  10453  recgt1i  10492  recreclt  10494  ledivp1i  10521  nngt0  10627  nnrecgt0  10636  elnnnn0c  10905  elnnz1  10953  recnz  11001  uz3m2nn  11191  xrub  11587  1mod  12123  expubnd  12327  expnbnd  12395  expnlbnd  12396  resqrex  13325  sin02gt0  14257  prmlem1  15090  prmlem2  15102  lsmss2  17329  ovolicopnf  22489  voliunlem3  22517  volsup  22521  volivth  22577  itg2seq  22712  itg2monolem2  22721  reeff1olem  23413  sinq12gt0  23474  logdivlti  23581  logdivlt  23582  efexple  24221  axlowdimlem16  24999  axlowdimlem17  25000  axlowdim  25003  dmdbr2  27968  dfon2lem3  30437  dfon2lem7  30441  frind  30487  nn0prpwlem  30984  tan2h  31939  mblfinlem4  31982  m1mod0mod1  38814  iccpartgt  38832  gbegt5  38953  gbogt5  38954  sgoldbalt  38973  nnsum4primesodd  38982  nnsum4primesoddALTV  38983  evengpoap3  38985  nnsum4primesevenALTV  38987  pfx2  39046  rusgr1vtx  39705  m1modmmod  40649  difmodm1lt  40650  regt1loggt0  40672  rege1logbrege0  40694  rege1logbzge0  40695
  Copyright terms: Public domain W3C validator