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  8982  reclt1  9228  crap0  9290  nominpos  9547  expnass  11095  crim  11637  sqrt00  11820  mulcn2  12094  sin02gt0  12547  opoe  12678  oddprm  13058  pythagtriplem3  13066  pc1  13104  prmlem0  13240  txswaphmeo  15471  sinq34lt0t  15982  cosordlem  16000  ppiqub  16194  lgsne0  16255  lgsdinn0  16265  eupth2lem3lem4fi  16812  3dom  17116