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  6398  2dom  6979  phplem4  7040  fiintim  7122  mulidnq  7608  nq0m0r  7675  nq0a0  7676  addpinq1  7683  0idsr  7986  1idsr  7987  00sr  7988  addresr  8056  mulresr  8057  pitonnlem2  8066  ax0id  8097  recexaplem2  8831  reclt1  9075  crap0  9137  nominpos  9381  expnass  10906  crim  11418  sqrt00  11600  mulcn2  11872  sin02gt0  12324  opoe  12455  oddprm  12831  pythagtriplem3  12839  pc1  12877  txswaphmeo  15044  sinq34lt0t  15554  cosordlem  15572  lgsne0  15766  lgsdinn0  15776  3dom  16587