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  8717  recgt1i  8752  recreclt  8754  nngt0  8841  nnrecgt0  8854  elnnnn0c  9118  elnnz1  9173  recnz  9240  uz3m2nn  9467  ledivge1le  9615  expubnd  10458  expnbnd  10523  expnlbnd  10524  sin02gt0  11642  oddge22np1  11753  dvdsnprmd  11982  reeff1olem  13052  sinq12gt0  13111  logdivlti  13162