Theorem mpan2i 713

Description: An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Hypotheses

Ref	Expression
mpan2i.1	|- ch
mpan2i.2	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Assertion

Ref	Expression
mpan2i	|- ( ph -> ( ps -> th ) )

Proof of Theorem mpan2i

Step	Hyp	Ref	Expression
1		mpan2i.1	. . 3 |- ch
2	1	a1i 11	. 2 |- ( ph -> ch )
3		mpan2i.2	. 2 |- ( ph -> ( ( ps /\ ch ) -> th ) )
4	2, 3	mpan2d 710	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  tcwf  8746  cflecard  9075  sqrlem7  13989  setciso  16741  lsmss1  18079  sincosq1lem  24249  pjcompi  28531  mdsl1i  29180  dfon2lem3  31690  dfon2lem7  31694  tan2h  33401  dvasin  33496  ismrc  37264  nnsum4primes4  41677  nnsum4primesprm  41679  nnsum4primesgbe  41681  nnsum4primesle9  41683  rngciso  41982  rngcisoALTV  41994  ringciso  42033  ringcisoALTV  42057  aacllem  42547