Theorem mpanr12 439

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 437	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	mpan2 425	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  6386  2dom  6966  phplem4  7024  fiintim  7104  mulidnq  7587  nq0m0r  7654  nq0a0  7655  addpinq1  7662  0idsr  7965  1idsr  7966  00sr  7967  addresr  8035  mulresr  8036  pitonnlem2  8045  ax0id  8076  recexaplem2  8810  reclt1  9054  crap0  9116  nominpos  9360  expnass  10879  crim  11385  sqrt00  11567  mulcn2  11839  sin02gt0  12291  opoe  12422  oddprm  12798  pythagtriplem3  12806  pc1  12844  txswaphmeo  15011  sinq34lt0t  15521  cosordlem  15539  lgsne0  15733  lgsdinn0  15743  3dom  16439