Theorem mpanr12 443

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  cnvoprab  6474  2dom  7097  phplem4  7160  fiintim  7242  mulidnq  7762  nq0m0r  7829  nq0a0  7830  addpinq1  7837  0idsr  8140  1idsr  8141  00sr  8142  addresr  8210  mulresr  8211  pitonnlem2  8220  ax0id  8251  recexaplem2  8988  reclt1  9234  crap0  9296  nominpos  9554  expnass  11103  crim  11645  sqrt00  11828  mulcn2  12103  sin02gt0  12556  opoe  12687  oddprm  13067  pythagtriplem3  13075  pc1  13113  prmlem0  13249  txswaphmeo  15547  sinq34lt0t  16058  cosordlem  16077  ppiqub  16293  bposlem9  16319  lgsne0  16362  lgsdinn0  16372  eupth2lem3lem4fi  16919  3dom  17223