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  3454  ordtri2orexmid  4570  opthreg  4603  ordtri2or2exmid  4618  ontri2orexmidim  4619  fvtp1  5794  nq0m0r  7568  nq02m  7577  gt0srpr  7860  map2psrprg  7917  pitoregt0  7961  axcnre  7993  addgt0  8520  addgegt0  8521  addgtge0  8522  addge0  8523  addgt0i  8560  addge0i  8561  addgegt0i  8562  add20i  8564  mulge0i  8692  recextlem1  8723  recap0  8757  recdivap  8790  recgt1  8969  prodgt0i  8980  prodge0i  8981  iccshftri  10116  iccshftli  10118  iccdili  10120  icccntri  10122  mulexpzap  10722  expaddzap  10726  m1expeven  10729  iexpcyc  10787  amgm2  11371  ege2le3  11924  sqnprm  12400  lmres  14662  2logb9irrap  15391