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  6399  2dom  6980  phplem4  7041  fiintim  7123  mulidnq  7609  nq0m0r  7676  nq0a0  7677  addpinq1  7684  0idsr  7987  1idsr  7988  00sr  7989  addresr  8057  mulresr  8058  pitonnlem2  8067  ax0id  8098  recexaplem2  8832  reclt1  9076  crap0  9138  nominpos  9382  expnass  10907  crim  11419  sqrt00  11601  mulcn2  11873  sin02gt0  12326  opoe  12457  oddprm  12833  pythagtriplem3  12841  pc1  12879  txswaphmeo  15047  sinq34lt0t  15557  cosordlem  15575  lgsne0  15769  lgsdinn0  15779  3dom  16590