Theorem mpani 434

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 9	. 2 |- ( ph -> ps )
3		mpani.2	. 2 |- ( ph -> ( ( ps /\ ch ) -> th ) )
4	2, 3	mpand 433	1 |- ( ph -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mp2ani  436  mulgt1  9183  recgt1i  9218  recreclt  9220  nngt0  9308  nnrecgt0  9321  elnnnn0c  9587  elnnz1  9646  recnz  9718  uz3m2nn  9952  ledivge1le  10106  expubnd  11011  expnbnd  11079  expnlbnd  11080  sin02gt0  12509  oddge22np1  12626  dvdsnprmd  12881  reeff1olem  15795  sinq12gt0  15854  logdivlti  15905  gausslemma2dlem4  16097