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  6235  2dom  6805  phplem4  6855  fiintim  6928  mulidnq  7388  nq0m0r  7455  nq0a0  7456  addpinq1  7463  0idsr  7766  1idsr  7767  00sr  7768  addresr  7836  mulresr  7837  pitonnlem2  7846  ax0id  7877  recexaplem2  8609  reclt1  8853  crap0  8915  nominpos  9156  expnass  10626  crim  10867  sqrt00  11049  mulcn2  11320  sin02gt0  11771  opoe  11900  oddprm  12259  pythagtriplem3  12267  pc1  12305  txswaphmeo  13824  sinq34lt0t  14255  cosordlem  14273  lgsne0  14442  lgsdinn0  14452