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  4812  dif20el  6937  domunfican  7576  mulgt1  10180  recgt1i  10221  recreclt  10223  ledivp1i  10250  nngt0  10343  nnrecgt0  10351  elnnnn0c  10617  elnnz1  10664  recnz  10709  xrub  11266  1mod  11732  expubnd  11916  expnbnd  11985  expnlbnd  11986  resqrex  12732  sin02gt0  13468  prmlem1  14127  prmlem2  14139  lsmss2  16156  ovolicopnf  20982  voliunlem3  21008  volsup  21012  volivth  21062  itg2seq  21195  itg2monolem2  21204  reeff1olem  21886  sinq12gt0  21944  logdivlti  22044  logdivlt  22045  efexple  22595  axlowdimlem16  23154  axlowdimlem17  23155  axlowdim  23158  dmdbr2  25658  dfon2lem3  27549  dfon2lem7  27553  wfi  27619  frind  27655  tan2h  28377  mblfinlem4  28384  nn0prpwlem  28470  uz3m2nn  30148