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  6343  2dom  6921  phplem4  6977  fiintim  7054  mulidnq  7537  nq0m0r  7604  nq0a0  7605  addpinq1  7612  0idsr  7915  1idsr  7916  00sr  7917  addresr  7985  mulresr  7986  pitonnlem2  7995  ax0id  8026  recexaplem2  8760  reclt1  9004  crap0  9066  nominpos  9310  expnass  10827  crim  11284  sqrt00  11466  mulcn2  11738  sin02gt0  12190  opoe  12321  oddprm  12697  pythagtriplem3  12705  pc1  12743  txswaphmeo  14908  sinq34lt0t  15418  cosordlem  15436  lgsne0  15630  lgsdinn0  15640