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  6320  2dom  6897  phplem4  6952  fiintim  7028  mulidnq  7502  nq0m0r  7569  nq0a0  7570  addpinq1  7577  0idsr  7880  1idsr  7881  00sr  7882  addresr  7950  mulresr  7951  pitonnlem2  7960  ax0id  7991  recexaplem2  8725  reclt1  8969  crap0  9031  nominpos  9275  expnass  10790  crim  11169  sqrt00  11351  mulcn2  11623  sin02gt0  12075  opoe  12206  oddprm  12582  pythagtriplem3  12590  pc1  12628  txswaphmeo  14793  sinq34lt0t  15303  cosordlem  15321  lgsne0  15515  lgsdinn0  15525