Theorem mpanl12 432

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 430	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 4	mpan 420	1 |- ( ch -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  reuun1  3358  ordtri2orexmid  4438  opthreg  4471  ordtri2or2exmid  4486  fvtp1  5631  nq0m0r  7264  nq02m  7273  gt0srpr  7556  map2psrprg  7613  pitoregt0  7657  axcnre  7689  addgt0  8210  addgegt0  8211  addgtge0  8212  addge0  8213  addgt0i  8250  addge0i  8251  addgegt0i  8252  add20i  8254  mulge0i  8382  recextlem1  8412  recap0  8445  recdivap  8478  recgt1  8655  prodgt0i  8666  prodge0i  8667  iccshftri  9778  iccshftli  9780  iccdili  9782  icccntri  9784  mulexpzap  10333  expaddzap  10337  m1expeven  10340  iexpcyc  10397  amgm2  10890  ege2le3  11377  sqnprm  11816  lmres  12417