Theorem mpanr12 433

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  cnvoprab  6061  2dom  6629  phplem4  6678  fiintim  6746  mulidnq  7098  nq0m0r  7165  nq0a0  7166  addpinq1  7173  0idsr  7463  1idsr  7464  00sr  7465  addresr  7524  mulresr  7525  pitonnlem2  7534  ax0id  7563  recexaplem2  8274  reclt1  8512  crap0  8574  nominpos  8809  expnass  10239  crim  10471  sqrt00  10652  mulcn2  10920  sin02gt0  11268  opoe  11387