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  6408  2dom  7023  phplem4  7084  fiintim  7166  mulidnq  7669  nq0m0r  7736  nq0a0  7737  addpinq1  7744  0idsr  8047  1idsr  8048  00sr  8049  addresr  8117  mulresr  8118  pitonnlem2  8127  ax0id  8158  recexaplem2  8891  reclt1  9135  crap0  9197  nominpos  9441  expnass  10970  crim  11498  sqrt00  11680  mulcn2  11952  sin02gt0  12405  opoe  12536  oddprm  12912  pythagtriplem3  12920  pc1  12958  txswaphmeo  15132  sinq34lt0t  15642  cosordlem  15660  lgsne0  15857  lgsdinn0  15867  eupth2lem3lem4fi  16414  3dom  16708