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  4924  dif20el  7054  domunfican  7694  mulgt1  10298  recgt1i  10339  recreclt  10341  ledivp1i  10368  nngt0  10461  nnrecgt0  10469  elnnnn0c  10735  elnnz1  10782  recnz  10827  xrub  11384  1mod  11856  expubnd  12040  expnbnd  12109  expnlbnd  12110  resqrex  12857  sin02gt0  13593  prmlem1  14252  prmlem2  14264  lsmss2  16285  ovolicopnf  21138  voliunlem3  21165  volsup  21169  volivth  21219  itg2seq  21352  itg2monolem2  21361  reeff1olem  22043  sinq12gt0  22101  logdivlti  22201  logdivlt  22202  efexple  22752  axlowdimlem16  23354  axlowdimlem17  23355  axlowdim  23358  dmdbr2  25858  dfon2lem3  27741  dfon2lem7  27745  wfi  27811  frind  27847  tan2h  28571  mblfinlem4  28578  nn0prpwlem  28664  uz3m2nn  30342