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  6210  2dom  6779  phplem4  6829  fiintim  6902  mulidnq  7338  nq0m0r  7405  nq0a0  7406  addpinq1  7413  0idsr  7716  1idsr  7717  00sr  7718  addresr  7786  mulresr  7787  pitonnlem2  7796  ax0id  7827  recexaplem2  8557  reclt1  8799  crap0  8861  nominpos  9102  expnass  10568  crim  10809  sqrt00  10991  mulcn2  11262  sin02gt0  11713  opoe  11841  oddprm  12200  pythagtriplem3  12208  pc1  12246  txswaphmeo  13036  sinq34lt0t  13467  cosordlem  13485  lgsne0  13654  lgsdinn0  13664