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  7756  nq0m0r  7823  nq0a0  7824  addpinq1  7831  0idsr  8134  1idsr  8135  00sr  8136  addresr  8204  mulresr  8205  pitonnlem2  8214  ax0id  8245  recexaplem2  8980  reclt1  9226  crap0  9288  nominpos  9543  expnass  11082  crim  11623  sqrt00  11806  mulcn2  12078  sin02gt0  12531  opoe  12662  oddprm  13038  pythagtriplem3  13046  pc1  13084  txswaphmeo  15422  sinq34lt0t  15932  cosordlem  15950  lgsne0  16157  lgsdinn0  16167  eupth2lem3lem4fi  16714  3dom  17018