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  6301  2dom  6873  phplem4  6925  fiintim  7001  mulidnq  7473  nq0m0r  7540  nq0a0  7541  addpinq1  7548  0idsr  7851  1idsr  7852  00sr  7853  addresr  7921  mulresr  7922  pitonnlem2  7931  ax0id  7962  recexaplem2  8696  reclt1  8940  crap0  9002  nominpos  9246  expnass  10754  crim  11040  sqrt00  11222  mulcn2  11494  sin02gt0  11946  opoe  12077  oddprm  12453  pythagtriplem3  12461  pc1  12499  txswaphmeo  14641  sinq34lt0t  15151  cosordlem  15169  lgsne0  15363  lgsdinn0  15373