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 )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  cnvoprab  6460  2dom  7083  phplem4  7146  fiintim  7228  mulidnq  7746  nq0m0r  7813  nq0a0  7814  addpinq1  7821  0idsr  8124  1idsr  8125  00sr  8126  addresr  8194  mulresr  8195  pitonnlem2  8204  ax0id  8235  recexaplem2  8970  reclt1  9216  crap0  9278  nominpos  9522  expnass  11060  crim  11601  sqrt00  11784  mulcn2  12056  sin02gt0  12509  opoe  12640  oddprm  13016  pythagtriplem3  13024  pc1  13062  txswaphmeo  15345  sinq34lt0t  15855  cosordlem  15873  lgsne0  16071  lgsdinn0  16081  eupth2lem3lem4fi  16628  3dom  16932