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  4621  dif20el  6686  domunfican  7316  mulgt1  9802  recgt1i  9840  recreclt  9842  ledivp1i  9869  nngt0  9962  nnrecgt0  9970  elnnnn0c  10198  elnnz1  10240  recnz  10278  xrub  10823  1mod  11201  expubnd  11368  expnbnd  11436  expnlbnd  11437  resqrex  11984  sin02gt0  12721  prmlem1  13358  prmlem2  13370  lsmss2  15228  ovolicopnf  19288  voliunlem3  19314  volsup  19318  volivth  19367  itg2seq  19502  itg2monolem2  19511  reeff1olem  20230  sinq12gt0  20283  logdivlti  20383  logdivlt  20384  efexple  20933  dmdbr2  23655  dfon2lem3  25166  dfon2lem7  25170  wfi  25232  frind  25268  axlowdimlem16  25611  axlowdimlem17  25612  axlowdim  25615  nn0prpwlem  26017
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