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  6287  2dom  6859  phplem4  6911  fiintim  6985  mulidnq  7449  nq0m0r  7516  nq0a0  7517  addpinq1  7524  0idsr  7827  1idsr  7828  00sr  7829  addresr  7897  mulresr  7898  pitonnlem2  7907  ax0id  7938  recexaplem2  8671  reclt1  8915  crap0  8977  nominpos  9220  expnass  10716  crim  11002  sqrt00  11184  mulcn2  11455  sin02gt0  11907  opoe  12036  oddprm  12397  pythagtriplem3  12405  pc1  12443  txswaphmeo  14489  sinq34lt0t  14966  cosordlem  14984  lgsne0  15154  lgsdinn0  15164