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  6394  2dom  6975  phplem4  7036  fiintim  7116  mulidnq  7599  nq0m0r  7666  nq0a0  7667  addpinq1  7674  0idsr  7977  1idsr  7978  00sr  7979  addresr  8047  mulresr  8048  pitonnlem2  8057  ax0id  8088  recexaplem2  8822  reclt1  9066  crap0  9128  nominpos  9372  expnass  10897  crim  11409  sqrt00  11591  mulcn2  11863  sin02gt0  12315  opoe  12446  oddprm  12822  pythagtriplem3  12830  pc1  12868  txswaphmeo  15035  sinq34lt0t  15545  cosordlem  15563  lgsne0  15757  lgsdinn0  15767  3dom  16523