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  7099  phplem4  7162  fiintim  7244  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  11102  crim  11644  sqrt00  11827  mulcn2  12102  sin02gt0  12555  opoe  12686  oddprm  13066  pythagtriplem3  13074  pc1  13112  prmlem0  13248  txswaphmeo  15564  sinq34lt0t  16075  cosordlem  16094  ppiqub  16310  bposlem9  16336  lgsne0  16379  lgsdinn0  16389  eupth2lem3lem4fi  16936  3dom  17240