Theorem mpani 427

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mp2ani  429  mulgt1  8645  recgt1i  8680  recreclt  8682  nngt0  8769  nnrecgt0  8782  elnnnn0c  9046  elnnz1  9101  recnz  9168  uz3m2nn  9395  ledivge1le  9543  expubnd  10381  expnbnd  10446  expnlbnd  10447  sin02gt0  11506  oddge22np1  11614  dvdsnprmd  11842  reeff1olem  12900  sinq12gt0  12959  logdivlti  13010