Theorem mpanr12 439

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  cnvoprab  6322  2dom  6899  phplem4  6954  fiintim  7030  mulidnq  7504  nq0m0r  7571  nq0a0  7572  addpinq1  7579  0idsr  7882  1idsr  7883  00sr  7884  addresr  7952  mulresr  7953  pitonnlem2  7962  ax0id  7993  recexaplem2  8727  reclt1  8971  crap0  9033  nominpos  9277  expnass  10792  crim  11202  sqrt00  11384  mulcn2  11656  sin02gt0  12108  opoe  12239  oddprm  12615  pythagtriplem3  12623  pc1  12661  txswaphmeo  14826  sinq34lt0t  15336  cosordlem  15354  lgsne0  15548  lgsdinn0  15558