Theorem mpanl12 412

Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)

Hypotheses

Ref	Expression
mpanl12.1	|- ph
mpanl12.2	|- ps
mpanl12.3	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Assertion

Ref	Expression
mpanl12	|- ( ch -> th )

Proof of Theorem mpanl12

Step	Hyp	Ref	Expression
1		mpanl12.2	. 2 |- ps
2		mpanl12.1	. . 3 |- ph
3		mpanl12.3	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	2, 3	mpanl1 410	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 4	mpan 400	1 |- ( ch -> th )

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  reuun1  3219  ordtri2orexmid  4248  opthreg  4280  ordtri2or2exmid  4296  fvtp1  5372  nq0m0r  6554  nq02m  6563  gt0srpr  6833  pitoregt0  6925  axcnre  6955  addgt0  7443  addgegt0  7444  addgtge0  7445  addge0  7446  addgt0i  7480  addge0i  7481  addgegt0i  7482  add20i  7484  mulge0i  7611  recextlem1  7632  recap0  7664  recdivap  7694  recgt1  7863  prodgt0i  7874  prodge0i  7875  iccshftri  8863  iccshftli  8865  iccdili  8867  icccntri  8869  mulexpzap  9295  expaddzap  9299  amgm2  9714