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  6380  2dom  6958  phplem4  7016  fiintim  7093  mulidnq  7576  nq0m0r  7643  nq0a0  7644  addpinq1  7651  0idsr  7954  1idsr  7955  00sr  7956  addresr  8024  mulresr  8025  pitonnlem2  8034  ax0id  8065  recexaplem2  8799  reclt1  9043  crap0  9105  nominpos  9349  expnass  10867  crim  11369  sqrt00  11551  mulcn2  11823  sin02gt0  12275  opoe  12406  oddprm  12782  pythagtriplem3  12790  pc1  12828  txswaphmeo  14995  sinq34lt0t  15505  cosordlem  15523  lgsne0  15717  lgsdinn0  15727