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  6301  2dom  6873  phplem4  6925  fiintim  7001  mulidnq  7475  nq0m0r  7542  nq0a0  7543  addpinq1  7550  0idsr  7853  1idsr  7854  00sr  7855  addresr  7923  mulresr  7924  pitonnlem2  7933  ax0id  7964  recexaplem2  8698  reclt1  8942  crap0  9004  nominpos  9248  expnass  10756  crim  11042  sqrt00  11224  mulcn2  11496  sin02gt0  11948  opoe  12079  oddprm  12455  pythagtriplem3  12463  pc1  12501  txswaphmeo  14665  sinq34lt0t  15175  cosordlem  15193  lgsne0  15387  lgsdinn0  15397