Theorem mpanr12 435

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 433	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	mpan2 421	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  6124  2dom  6692  phplem4  6742  fiintim  6810  mulidnq  7190  nq0m0r  7257  nq0a0  7258  addpinq1  7265  0idsr  7568  1idsr  7569  00sr  7570  addresr  7638  mulresr  7639  pitonnlem2  7648  ax0id  7679  recexaplem2  8406  reclt1  8647  crap0  8709  nominpos  8950  expnass  10391  crim  10623  sqrt00  10805  mulcn2  11074  sin02gt0  11459  opoe  11581  txswaphmeo  12479  sinq34lt0t  12901  cosordlem  12919