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

Theorem mpani 680
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 679 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  mp2ani  682  wfi  5432  ordelinel  5540  dif20el  7218  domunfican  7853  mulgt1  10471  recgt1i  10510  recreclt  10512  ledivp1i  10539  nngt0  10645  nnrecgt0  10654  elnnnn0c  10922  elnnz1  10970  recnz  11018  uz3m2nn  11208  xrub  11604  1mod  12135  expubnd  12339  expnbnd  12407  expnlbnd  12408  resqrex  13314  sin02gt0  14245  prmlem1  15078  prmlem2  15090  lsmss2  17317  ovolicopnf  22476  voliunlem3  22503  volsup  22507  volivth  22563  itg2seq  22698  itg2monolem2  22707  reeff1olem  23399  sinq12gt0  23460  logdivlti  23567  logdivlt  23568  efexple  24207  axlowdimlem16  24985  axlowdimlem17  24986  axlowdim  24989  dmdbr2  27954  dfon2lem3  30438  dfon2lem7  30442  frind  30488  nn0prpwlem  30983  tan2h  31901  mblfinlem4  31944  m1mod0mod1  38593  iccpartgt  38611  gbegt5  38732  gbogt5  38733  sgoldbalt  38752  nnsum4primesodd  38761  nnsum4primesoddALTV  38762  evengpoap3  38764  nnsum4primesevenALTV  38766  pfx2  38823  m1modmmod  39945  difmodm1lt  39946  regt1loggt0  39968  rege1logbrege0  39990  rege1logbzge0  39991
  Copyright terms: Public domain W3C validator