Theorem mpanl12 436

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 434	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 4	mpan 424	1 |- ( ch -> 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:  reuun1  3503  ordtri2orexmid  4645  opthreg  4678  ordtri2or2exmid  4693  ontri2orexmidim  4694  fvtp1  5895  nq0m0r  7771  nq02m  7780  gt0srpr  8063  map2psrprg  8120  pitoregt0  8164  axcnre  8196  addgt0  8722  addgegt0  8723  addgtge0  8724  addge0  8725  addgt0i  8762  addge0i  8763  addgegt0i  8764  add20i  8766  mulge0i  8894  recextlem1  8925  recap0  8959  recdivap  8992  recgt1  9171  prodgt0i  9182  prodge0i  9183  iccshftri  10328  iccshftli  10330  iccdili  10332  icccntri  10334  mulexpzap  10941  expaddzap  10945  m1expeven  10948  iexpcyc  11006  amgm2  11803  ege2le3  12357  sqnprm  12833  lmres  15113  2logb9irrap  15842