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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mp2ani  436  mulgt1  9201  recgt1i  9236  recreclt  9238  nngt0  9338  nnrecgt0  9351  elnnnn0c  9619  elnnz1  9678  recnz  9750  uz3m2nn  9989  ledivge1le  10144  expubnd  11054  expnbnd  11122  expnlbnd  11123  sin02gt0  12556  oddge22np1  12673  dvdsnprmd  12928  prmlem1  13251  prmlem2  13263  reeff1olem  15997  sinq12gt0  16057  logdivlti  16111  gausslemma2dlem4  16388