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

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 657	1 |- ( ph -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 359

This theorem is referenced by:  mp2ani  660  ordelinel  4639  dif20el  6708  domunfican  7338  mulgt1  9825  recgt1i  9863  recreclt  9865  ledivp1i  9892  nngt0  9985  nnrecgt0  9993  elnnnn0c  10221  elnnz1  10263  recnz  10301  xrub  10846  1mod  11228  expubnd  11395  expnbnd  11463  expnlbnd  11464  resqrex  12011  sin02gt0  12748  prmlem1  13385  prmlem2  13397  lsmss2  15255  ovolicopnf  19373  voliunlem3  19399  volsup  19403  volivth  19452  itg2seq  19587  itg2monolem2  19596  reeff1olem  20315  sinq12gt0  20368  logdivlti  20468  logdivlt  20469  efexple  21018  dmdbr2  23759  dfon2lem3  25355  dfon2lem7  25359  wfi  25421  frind  25457  axlowdimlem16  25800  axlowdimlem17  25801  axlowdim  25804  mblfinlem3  26145  nn0prpwlem  26215

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