Theorem mpanr12 437

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 435	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	mpan2 423	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  cnvoprab  6213  2dom  6783  phplem4  6833  fiintim  6906  mulidnq  7351  nq0m0r  7418  nq0a0  7419  addpinq1  7426  0idsr  7729  1idsr  7730  00sr  7731  addresr  7799  mulresr  7800  pitonnlem2  7809  ax0id  7840  recexaplem2  8570  reclt1  8812  crap0  8874  nominpos  9115  expnass  10581  crim  10822  sqrt00  11004  mulcn2  11275  sin02gt0  11726  opoe  11854  oddprm  12213  pythagtriplem3  12221  pc1  12259  txswaphmeo  13115  sinq34lt0t  13546  cosordlem  13564  lgsne0  13733  lgsdinn0  13743