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  8758  recgt1i  8793  recreclt  8795  nngt0  8882  nnrecgt0  8895  elnnnn0c  9159  elnnz1  9214  recnz  9284  uz3m2nn  9511  ledivge1le  9662  expubnd  10512  expnbnd  10578  expnlbnd  10579  sin02gt0  11704  oddge22np1  11818  dvdsnprmd  12057  reeff1olem  13332  sinq12gt0  13391  logdivlti  13442