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  6430  2dom  7046  phplem4  7109  fiintim  7191  mulidnq  7704  nq0m0r  7771  nq0a0  7772  addpinq1  7779  0idsr  8082  1idsr  8083  00sr  8084  addresr  8152  mulresr  8153  pitonnlem2  8162  ax0id  8193  recexaplem2  8926  reclt1  9170  crap0  9232  nominpos  9476  expnass  11007  crim  11543  sqrt00  11725  mulcn2  11997  sin02gt0  12450  opoe  12581  oddprm  12957  pythagtriplem3  12965  pc1  13003  txswaphmeo  15186  sinq34lt0t  15696  cosordlem  15714  lgsne0  15911  lgsdinn0  15921  eupth2lem3lem4fi  16468  3dom  16762