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  6470  2dom  7093  phplem4  7156  fiintim  7238  mulidnq  7757  nq0m0r  7824  nq0a0  7825  addpinq1  7832  0idsr  8135  1idsr  8136  00sr  8137  addresr  8205  mulresr  8206  pitonnlem2  8215  ax0id  8246  recexaplem2  8983  reclt1  9229  crap0  9291  nominpos  9548  expnass  11097  crim  11639  sqrt00  11822  mulcn2  12097  sin02gt0  12550  opoe  12681  oddprm  13061  pythagtriplem3  13069  pc1  13107  prmlem0  13243  txswaphmeo  15513  sinq34lt0t  16024  cosordlem  16042  ppiqub  16254  bposlem9  16280  lgsne0  16323  lgsdinn0  16333  eupth2lem3lem4fi  16880  3dom  17184