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  6237  2dom  6807  phplem4  6857  fiintim  6930  mulidnq  7390  nq0m0r  7457  nq0a0  7458  addpinq1  7465  0idsr  7768  1idsr  7769  00sr  7770  addresr  7838  mulresr  7839  pitonnlem2  7848  ax0id  7879  recexaplem2  8611  reclt1  8855  crap0  8917  nominpos  9158  expnass  10628  crim  10869  sqrt00  11051  mulcn2  11322  sin02gt0  11773  opoe  11902  oddprm  12261  pythagtriplem3  12269  pc1  12307  txswaphmeo  13906  sinq34lt0t  14337  cosordlem  14355  lgsne0  14524  lgsdinn0  14534