Theorem mpanr12 439

Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)

Hypotheses

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

Assertion

Ref	Expression
mpanr12	|- ( ph -> th )

Proof of Theorem mpanr12

Step	Hyp	Ref	Expression
1		mpanr12.2	. 2 |- ch
2		mpanr12.1	. . 3 |- ps
3		mpanr12.3	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
4	2, 3	mpanr1 437	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	mpan2 425	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  cnvoprab  6399  2dom  6980  phplem4  7041  fiintim  7123  mulidnq  7609  nq0m0r  7676  nq0a0  7677  addpinq1  7684  0idsr  7987  1idsr  7988  00sr  7989  addresr  8057  mulresr  8058  pitonnlem2  8067  ax0id  8098  recexaplem2  8832  reclt1  9076  crap0  9138  nominpos  9382  expnass  10908  crim  11436  sqrt00  11618  mulcn2  11890  sin02gt0  12343  opoe  12474  oddprm  12850  pythagtriplem3  12858  pc1  12896  txswaphmeo  15064  sinq34lt0t  15574  cosordlem  15592  lgsne0  15786  lgsdinn0  15796  eupth2lem3lem4fi  16343  3dom  16638