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

Step	Hyp	Ref	Expression
1		mpani.1	. . 3 |- ps
2	1	a1i 11	. 2 |- ( ph -> ps )
3		mpani.2	. 2 |- ( ph -> ( ( ps /\ ch ) -> th ) )
4	2, 3	mpand 675	1 |- ( ph -> ( ch -> th ) )

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  4976  dif20el  7152  domunfican  7789  mulgt1  10397  recgt1i  10438  recreclt  10440  ledivp1i  10467  nngt0  10561  nnrecgt0  10569  elnnnn0c  10837  elnnz1  10886  recnz  10932  uz3m2nn  11120  xrub  11499  1mod  11992  expubnd  12190  expnbnd  12259  expnlbnd  12260  resqrex  13043  sin02gt0  13784  prmlem1  14447  prmlem2  14459  lsmss2  16482  ovolicopnf  21670  voliunlem3  21697  volsup  21701  volivth  21751  itg2seq  21884  itg2monolem2  21893  reeff1olem  22575  sinq12gt0  22633  logdivlti  22733  logdivlt  22734  efexple  23284  axlowdimlem16  23936  axlowdimlem17  23937  axlowdim  23940  dmdbr2  26898  dfon2lem3  28794  dfon2lem7  28798  wfi  28864  frind  28900  tan2h  29624  mblfinlem4  29631  nn0prpwlem  29717