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  6292  2dom  6864  phplem4  6916  fiintim  6992  mulidnq  7456  nq0m0r  7523  nq0a0  7524  addpinq1  7531  0idsr  7834  1idsr  7835  00sr  7836  addresr  7904  mulresr  7905  pitonnlem2  7914  ax0id  7945  recexaplem2  8679  reclt1  8923  crap0  8985  nominpos  9229  expnass  10737  crim  11023  sqrt00  11205  mulcn2  11477  sin02gt0  11929  opoe  12060  oddprm  12428  pythagtriplem3  12436  pc1  12474  txswaphmeo  14557  sinq34lt0t  15067  cosordlem  15085  lgsne0  15279  lgsdinn0  15289