Theorem mpanr12 430

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  cnvoprab  5934  2dom  6452  phplem4  6501  mulidnq  6851  nq0m0r  6918  nq0a0  6919  addpinq1  6926  0idsr  7216  1idsr  7217  00sr  7218  addresr  7277  mulresr  7278  pitonnlem2  7287  ax0id  7316  recexaplem2  8019  reclt1  8251  crap0  8312  nominpos  8545  expnass  9896  crim  10119  sqrt00  10300  mulcn2  10525  opoe  10675