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  6289  2dom  6861  phplem4  6913  fiintim  6987  mulidnq  7451  nq0m0r  7518  nq0a0  7519  addpinq1  7526  0idsr  7829  1idsr  7830  00sr  7831  addresr  7899  mulresr  7900  pitonnlem2  7909  ax0id  7940  recexaplem2  8673  reclt1  8917  crap0  8979  nominpos  9223  expnass  10719  crim  11005  sqrt00  11187  mulcn2  11458  sin02gt0  11910  opoe  12039  oddprm  12400  pythagtriplem3  12408  pc1  12446  txswaphmeo  14500  sinq34lt0t  15007  cosordlem  15025  lgsne0  15195  lgsdinn0  15205