Theorem mpanr12 436

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 434	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	mpan2 422	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  cnvoprab  6198  2dom  6767  phplem4  6817  fiintim  6890  mulidnq  7326  nq0m0r  7393  nq0a0  7394  addpinq1  7401  0idsr  7704  1idsr  7705  00sr  7706  addresr  7774  mulresr  7775  pitonnlem2  7784  ax0id  7815  recexaplem2  8545  reclt1  8787  crap0  8849  nominpos  9090  expnass  10556  crim  10796  sqrt00  10978  mulcn2  11249  sin02gt0  11700  opoe  11828  oddprm  12187  pythagtriplem3  12195  pc1  12233  txswaphmeo  12921  sinq34lt0t  13352  cosordlem  13370  lgsne0  13539  lgsdinn0  13549