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  4985  dif20el  7173  domunfican  7811  mulgt1  10422  recgt1i  10462  recreclt  10464  ledivp1i  10491  nngt0  10585  nnrecgt0  10594  elnnnn0c  10862  elnnz1  10911  recnz  10959  uz3m2nn  11148  xrub  11528  1mod  12031  expubnd  12229  expnbnd  12298  expnlbnd  12299  resqrex  13096  sin02gt0  13939  prmlem1  14605  prmlem2  14617  lsmss2  16813  ovolicopnf  22061  voliunlem3  22088  volsup  22092  volivth  22142  itg2seq  22275  itg2monolem2  22284  reeff1olem  22967  sinq12gt0  23026  logdivlti  23131  logdivlt  23132  efexple  23682  axlowdimlem16  24387  axlowdimlem17  24388  axlowdim  24391  dmdbr2  27349  dfon2lem3  29434  dfon2lem7  29438  wfi  29504  frind  29540  tan2h  30252  mblfinlem4  30259  nn0prpwlem  30345  pfx2  32530