Theorem mpanr12 415

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

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  2dom  6285  phplem4  6318  mulidnq  6487  nq0m0r  6554  nq0a0  6555  addpinq1  6562  0idsr  6852  1idsr  6853  00sr  6854  addresr  6913  mulresr  6914  pitonnlem2  6923  ax0id  6952  recexaplem2  7633  reclt1  7862  crap0  7910  nominpos  8162  expnass  9357  crim  9458  sqrt00  9638  mulcn2  9833